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