proposition: Lemma bet_ts__ts : forall A B X Y Z, TS A B X Y -> Bet X Y Z -> TS A B X Z.
proof: Proof. intros A B X Y Z [HNCol1 [HNCol2 [T [HT1 HT2]]]] HBet. repeat split; trivial. intro; assert (Z = T); [apply (l6_21 A B X Y); Col; intro|]; treat_equalities; auto. exists T; split; eBetween. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar