proposition: Lemma bet2_le2__le1245 : forall A B C A' B' C', Bet A B C -> Bet A' B' C' -> Le B C B' C' -> Le A' C' A C -> Le A' B' A B.
proof: Proof. intros A B C A' B' C'; intros. apply le_comm. apply (bet2_le2__le2356 C _ _ C'); Le; Between. Qed.
imports: GeoCoq.Tarski_dev.Ch05_bet_le