fof(th_2n_01,axiom,(![L,A,P1,P2]:(line(L)&point(A)&plane(P1)&plane(P2)&ninc_po_l(A,L)&inc_po_pl(A,P1)&inc_l_pl(L,P1)&inc_po_pl(A,P2)&inc_l_pl(L,P2))=>(P1=P2))).
