proposition: Lemma bet__ts : forall A B X Y, A <> Y -> ~ Col A B X -> Bet X A Y -> TS A B X Y.
proof: Proof. intros A B X Y HAY HNCol HBet. repeat split; Col. intro; apply HNCol, col_transitivity_1 with Y; Col. exists A; split; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar