assume [A,B]: (point(A) & point(B) & A!=B)
let [L1,D] : (line(L1) & point(D) & inc_po_l(A,L1) & inc_po_l(B,L1) & ninc_po_l(D,L1))
let [E] : (point(E) & bet(B,D,E))
let [F] : (point(F) & bet(A,E,F))
have (ncol(A,B,E))
have (F!=D)
let [L2] : (line(L2) & inc_po_l(F,L2) & inc_po_l(D,L2))
have (ninc_po_l(A,L2))
let [P] : (plane(P) & inc_po_pl(A,P) & inc_po_pl(B,P) & inc_po_pl(E,P))
have (inc_po_pl(D,P))
have (inc_po_pl(F,P))
have (inc_l_pl(L2,P))
have (pash(A,B,E,L2,P))
have (E!=A)
let [L3] : (line(L3) & inc_po_l(E,L3) & inc_po_l(A,L3))
have (L3!=L2)
have (cut(L2,A,B))
let [C] : (point(C) & bet(A,C,B))
   


