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))

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

infer (col(A,B,C) | ncol(A,B,C))

  case (col(A,B,C))
  infer (inc_po_l(A,L))
  lookup contradiction

  case (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(L,P))
  lookup goal
