proposition: Lemma T_dec : forall A B C, T A B C \/ ~ T A B C.
proof: Proof. intros A B C. elim (bet_dec A B C); intro HBet. left; apply Bet_T; assumption. right; intro HT; apply HBet; apply T_Bet in HT; assumption. Qed.
imports: GeoCoq.Axioms.beeson_s_axioms GeoCoq.Tarski_dev.Ch08_orthogonality