fof(goal, conjecture,(![L1,L2,A,B,C,P]:((line(L1)&line(L2)&int_l_l(L1,L2)&point(A)&inc_po_l(A,L1)&inc_po_l(A,L2)&point(B)&B!=A&inc_po_l(B,L1)&point(C)&C!=A&inc_po_l(C,L2)&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))))).
