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