proposition: Lemma l9_41_1 : forall A B C P Q R, TSP A B C P R -> TSP A B C Q R -> OSP A B C P Q.
proof: Proof. intros A B C P Q R H1 H2. exists R; split; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar