proposition: Lemma BetT_symmetry : forall A B C, BetT A B C -> BetT C B A.
proof: Proof. intros. unfold BetT in *. intuition. left. apply Ibetween_symmetry. assumption. Qed.
imports: GeoCoq.Axioms.beeson_s_axioms GeoCoq.Axioms.tarski_axioms Classical