proposition: Lemma image_preserves_out : forall X Y A B C A' B' C', Out A B C -> Reflect A A' X Y -> Reflect B B' X Y -> Reflect C C' X Y -> Out A' B' C'.
proof: Proof. intros. unfold Out in *. spliter. repeat split; auto. intro. subst B'. assert(B = A). apply (l10_2_uniqueness X Y A' B A H1 H0). contradiction. intro. subst C'. assert(C=A). apply (l10_2_uniqueness X Y A' C A H2 H0). contradiction. induction H4. left. apply (image_preserves_bet1 X Y A B C); auto. right. apply (image_preserves_bet1 X Y A C B); auto. Qed.
imports: GeoCoq.Tarski_dev.Ch14_order