proposition: Lemma l9_4_2 : forall P Q A C R S U V, TS P Q A C -> Col R P Q -> Perp P Q A R -> Col S P Q -> Perp P Q C S -> Out R U A -> Out S V C -> TS P Q U V.
proof: Proof. intros. assert(Le S C R A \/ Le R A S C) by (apply le_cases). induction H6. eapply l9_4_2_aux with A C R S;assumption. apply l9_2. apply l9_2 in H. eapply l9_4_2_aux with C A S R;auto. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar