fof(th_6c_06,axiom,(![L1,L2,L3,A,B,C,P]:((line(L1)&line(L2)&line(L3)&point(A)&point(B)&point(C)&L1!=L2&L2!=L3&L3!=L1&int_l_l(L1,L2)&int_l_l(L2,L3)&int_l_l(L3,L1)&inc_po_l(A,L1)&inc_po_l(A,L2)&ninc_po_l(A,L3)&ninc_po_l(B,L1)&inc_po_l(B,L2)&inc_po_l(B,L3)&inc_po_l(C,L1)&ninc_po_l(C,L2)&inc_po_l(C,L3)&A!=B&B!=C&C!=A&ncol(A,B,C)&plane(P)&inc_po_pl(A,P)&inc_po_pl(B,P)&inc_po_pl(C,P))=>(inc_l_pl(L1,P)&inc_l_pl(L2,P)&inc_l_pl(L3,P))))).
