assume [P1,P2,A] : (plane(P1) & plane(P2) & point(A) & P1!=P2 & inc_po_pl(A,P1) & inc_po_pl(A,P2))
goal construct [L] : (line(L) & inc_l_pl(L,P1) & inc_l_pl(L,P2))

construct [B] : (point(B) & A!=B & inc_po_pl(B,P1) & inc_po_pl(B,P2))
construct [L] : (line(L) & inc_po_l(A,L) & inc_po_l(B,L))
infer (inc_l_pl(L,P1) & inc_l_pl(L,P2))
lookup goal
