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