proposition: Lemma out_two_sides_two_sides : forall A B X Y P PX, A <> PX -> Col A B PX -> Out PX X P -> TS A B P Y -> TS A B X Y.
proof: Proof. intros. assert(OS A B P X). eapply (col_one_side _ PX). Col. unfold TS in H2. spliter. auto. intro. subst B. Col. apply invert_one_side. apply out_one_side. left. intro. unfold TS in H2. spliter. apply H2. ColR. apply l6_6. assumption. eapply l9_8_2. apply H2. assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar