fof(goal, conjecture,(![L,A,P1,P2,B,C]:((line(L)&point(A)&plane(P1)&plane(P2)&ninc_po_l(A,L)&inc_po_pl(A,P1)&inc_l_pl(L,P1)&inc_po_pl(A,P2)&inc_l_pl(L,P2)&point(B)&point(C)&B!=C&inc_po_l(B,L)&inc_po_l(C,L)&ncol(A,B,C))=>(inc_po_pl(A,P1)&inc_po_pl(B,P1)&inc_po_pl(C,P1)&inc_po_pl(A,P2)&inc_po_pl(B,P2)&inc_po_pl(C,P2))))).
