proposition: Lemma l9_9 : forall P Q A B, TS P Q A B -> ~ OS P Q A B.
proof: Proof. intros. intro. apply (l9_8_2 P Q A B B ) in H. apply not_two_sides_id in H. assumption. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar