assume [A,B,C,D,L,P1,P2] : (point(A) & point(B) & point(C) & point(D) & line(L) & plane(P1) & plane(P2) & A!=B & inc_po_l(A,L) & inc_po_l(B,L) & inc_po_l(C,L) & ncol(A,B,D) & ncol(A,C,D) & inc_po_pl(A,P1) & inc_po_pl(B,P1) & inc_po_pl(D,P1) & inc_po_pl(A,P2) & inc_po_pl(C,P2) & inc_po_pl(D,P2))
have (P1 = P2)
