proposition: Lemma l9_2 : forall A B P Q, TS A B P Q -> TS A B Q P.
proof: Proof. unfold TS. intros. spliter. repeat split; Col. destruct H1 as [T [HCol1 HCol2]]. exists T; Col; Between. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar