assume [L,A,P1,P2] : (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))
goal (P1 = P2)
construct [B,C] : (point(B) & point(C) & B!=C & inc_po_l(B,L) & inc_po_l(C,L))
infer (ncol(A,B,C))
infer (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))
infer (P1 = P2)
lookup goal
