proposition: Lemma l9_18 : forall X Y A B P, Col X Y P -> Col A B P -> (TS X Y A B <-> (Bet A P B /\ ~Col X Y A /\ ~Col X Y B)).
proof: Proof. intros. split. intros. unfold TS in H1. spliter. assert (X <> Y). intro. subst Y. spliter. Col. ex_and H3 T. assert (P=T). apply l6_21 with X Y A B; Col. intro. subst B. apply between_identity in H5. subst A. contradiction. subst T. repeat split; Col. intro. unfold TS. spliter. repeat split; Col. exists P. split. apply col_permutation_2. assumption. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar