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