proposition: Lemma BetT_id : forall A B, BetT A B A -> A=B.
proof: Proof. intros. unfold BetT in *. intuition. apply Ibetween_identity in H0. elim H0. Qed.
imports: GeoCoq.Axioms.beeson_s_axioms GeoCoq.Axioms.tarski_axioms Classical