proposition: Lemma T_Bet : forall A B C, T A B C -> Bet A B C.
proof: Proof. intros A B C HT. unfold T in HT. elim (bet_dec A B C); intro HBet. assumption. exfalso. apply HT. split. intro; subst; apply HBet; apply between_trivial2. split. intro; subst; apply HBet; apply between_trivial. intro HBetH; apply HBet; apply BetH_Bet in HBetH; assumption. Qed.
imports: GeoCoq.Axioms.beeson_s_axioms GeoCoq.Tarski_dev.Ch08_orthogonality