proposition: Lemma bet_id : forall A B : ITpoint, BetT A B A -> A = B.
proof: Proof. intros. unfold BetT in H. decompose [or] H. apply Ibetween_identity in H0. elim H0. assumption. intuition. Qed.
imports: GeoCoq.Axioms.beeson_s_axioms GeoCoq.Axioms.tarski_axioms Classical