assume [P,Q] : (line(P) & line(Q) & P != Q & int_l_l(P,Q))
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))

construct [R] : (plane(R) & inc_po_pl(A,R) & inc_po_pl(B,R) & inc_po_pl(C,R))
infer (inc_l_pl(P,R))
infer (inc_l_pl(Q,R))
lookup (inc_l_pl(P,R) & inc_l_pl(Q,R))
