proposition: Lemma l9_9_bis : forall P Q A B, OS P Q A B -> ~ TS P Q A B.
proof: Proof. intros. intro. unfold OS in H. ex_and H C. assert (OS P Q A B). eapply l9_8_1. apply H. assumption. assert (~ OS P Q A B). apply l9_9. assumption. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar