assume [A,B,C,D] : (point(A) & point(B) & point(C) & point(D) & bet(A,B,C) & bet(A,D,C))
let [L] : (line(L) & inc_po_l(A,L) & inc_po_l(B,L) & inc_po_l(C,L) & inc_po_l(D,L))
have (col(B,A,D))
have (nbet(B,A,D))
