assume [P,Q,R1,R2] : (line(P) & line(Q) & P != Q & int_l_l(P,Q) & plane(R1) & plane(R2) & inc_l_pl(P,R1) & inc_l_pl(P,R2) & inc_l_pl(Q,R1) & inc_l_pl(Q,R2))
construct [A] : (point(A) & inc_po_l(A,P) & inc_po_l(A,Q))
construct [B] : (point(B) & A!=B & inc_po_l(B,P))
construct [C] : (point(C) & A!=C & inc_po_l(C,Q))

infer (col(A,B,C) | ncol(A,B,C))

case (col(A,B,C))
infer (P = Q)
lookup contradiction

case (ncol(A,B,C))
infer (inc_po_pl(A,R1) & inc_po_pl(B,R1) & inc_po_pl(C,R1))
infer (inc_po_pl(A,R2) & inc_po_pl(B,R2) & inc_po_pl(C,R2))
lookup (R1=R2)
