assume [L1,L2] : (line(L1) & line(L2) & int_l_l(L1, L2))
goal (construct [P] : (plane(P) & inc_l_pl(L1,P) & inc_l_pl(L2,P)))

construct [A] : (point(A) & inc_po_l(A,L1) & inc_po_l(A,L2))
construct [B] : (point(B) & B != A & inc_po_l(B,L1))
construct [C] : (point(C) & C != A & inc_po_l(C,L2))
infer (ncol(A,B,C))
construct [P] : (plane(P) & inc_po_pl(A,P) & inc_po_pl(B,P) & inc_po_pl(C,P))
infer (inc_l_pl(L1,P) & inc_l_pl(L2,P))
lookup goal
