proposition: Lemma between_cong_3 : forall A B D E, A <> B -> Bet A B D -> Bet A B E -> Cong B D B E -> D = E.
proof: Proof. intros. assert (T:=l5_2 A B D E H H0 H1). elim T; intro; clear T. apply between_cong with B; Cong. symmetry; apply between_cong with B; Cong. Qed.
imports: GeoCoq.Tarski_dev.Ch04_col