proposition: Lemma ts_ts_os : forall A B C D, TS A B C D -> TS C D A B -> OS A C B D.
proof: Proof. intros. unfold TS in *. spliter. ex_and H4 T1. ex_and H2 T. assert(T1 = T). assert_cols. apply (l6_21 C D A B); Col. intro. subst B. Col. subst T1. assert(OS A C T B). apply(out_one_side A C T B). right. intro. Col. unfold Out. repeat split. intro. subst T. contradiction. intro. subst B. Col. left. assumption. assert(OS C A T D). apply(out_one_side C A T D). right. intro. apply H0. Col. unfold Out. repeat split. intro. subst T. contradiction. intro. subst D. Col. left. assumption. apply invert_one_side in H8. apply (one_side_transitivity A C B T). apply one_side_symmetry. assumption. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar