proposition: Lemma bet3__bet : forall A B C D E, Bet A B E -> Bet A D E -> Bet B C D -> Bet A C E.
proof: Proof. intros. destruct (l5_3 A B D E H H0). apply between_exchange4 with D; trivial. apply between_exchange2 with B; assumption. apply between_exchange4 with B; trivial. apply between_exchange2 with D; Between. Qed.
imports: GeoCoq.Tarski_dev.Ch04_col