proposition: Lemma image_preserves_bet : forall A B C A' B' C' X Y, ReflectL A A' X Y -> ReflectL B B' X Y -> ReflectL C C' X Y -> Bet A B C -> Bet A' B' C'.
proof: Proof. intros. destruct (eq_dec_points X Y). subst Y. apply image_spec__eq in H. apply image_spec__eq in H0. apply image_spec__eq in H1. subst; assumption. eapply l4_6. apply H2. unfold Cong_3. repeat split; apply l10_10_spec with X Y. apply l10_4_spec. apply H. apply l10_4_spec; assumption. apply l10_4_spec. apply H. apply l10_4_spec. assumption. apply l10_4_spec. apply H0. apply l10_4_spec. assumption. Qed.
imports: GeoCoq.Meta_theory.Dimension_axioms.upper_dim_2 GeoCoq.Tarski_dev.Ch10_line_reflexivity