proposition: Lemma l5_2 : forall A B C D, A <> B -> Bet A B C -> Bet A B D -> Bet B C D \/ Bet B D C.
proof: Proof. intros. assert (Bet A C D \/ Bet A D C) by (eapply l5_1; eauto). induction H2. left; eBetween. right; eBetween. Qed.
imports: GeoCoq.Tarski_dev.Ch04_col