fof(th_1n_01,axiom,(![L,A]:(line(L)&point(A)&ninc_po_l(A,L))=>(?[P]:(plane(P)&inc_po_pl(A,P)&inc_l_pl(L,P))))).
