proposition: Lemma symmetry_preseves_bet2 : forall A B M A' B', Midpoint M A A' -> Midpoint M B B' -> Bet M A' B' -> Bet M A B.
proof: Proof. intros. eapply l7_15. apply l7_3_2. apply l7_2. apply H. apply l7_2. apply H0. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel