proposition: Lemma bet_ts__os : forall A B X Y Z, TS A B X Y -> Bet X Y Z -> OS A B Y Z.
proof: Proof. intros A B X Y Z HTS HBet. exists X; split; apply l9_2; trivial. apply bet_ts__ts with Y; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar