proposition: Lemma l5_3 : forall A B C D, Bet A B D -> Bet A C D -> Bet A B C \/ Bet A C B.
proof: Proof. intros. assert (exists P, Bet D A P /\ A<>P) by (apply point_construction_different). ex_and H1 P. assert (Bet P A B) by eBetween. assert (Bet P A C) by eBetween. apply (l5_2 P);auto. Qed.
imports: GeoCoq.Tarski_dev.Ch04_col