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

construct [B,C] : (point(B) & point(C) & B!=C & inc_po_l(B,L) & inc_po_l(C,L))

infer (inc_po_l(A,L) | ninc_po_l(A,L))

  case (inc_po_l(A,L))  
  lookup goal

  case (ninc_po_l(A,L))
  infer (P1 = P2)
  lookup contradiction
  
