assume [P,Q] : (line(P) & line(Q) & P != Q & int_l_l(P,Q))
%goal (construct [R] : (plane(R) & inc_l_pl(P,R) & inc_l_pl(Q,R))
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 (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) & inc_l_pl(Q,R))
