assume [L,A] : (line(L) & point(A) & ninc_po_l(A,L))
goal (construct [P] : (plane(P) & inc_po_pl(A,P) & inc_l_pl(L,P)))
infer goal
