proposition: Lemma bet2__out : forall A B C B', A <> B -> A <> B' -> Bet A B C -> Bet A B' C -> Out A B B'.
proof: Proof. intros. apply bet2_out_out with C C; auto. apply bet_neq12__neq in H1; auto. apply out_trivial; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch05_bet_le