proposition: Lemma Bet_T : forall A B C, Bet A B C -> T A B C.
proof: Proof. intros A B C HBet. unfold T. intro HT. destruct HT as [HAB [HBC HNBet]]. apply HNBet. unfold BetH. intuition. Qed.
imports: GeoCoq.Axioms.beeson_s_axioms GeoCoq.Tarski_dev.Ch08_orthogonality