proposition: Lemma out_out_two_sides : forall A B X Y U V I, A <> B -> TS A B X Y -> Col I A B -> Col I X Y -> Out I X U -> Out I Y V -> TS A B U V.
proof: Proof. intros. unfold TS in *. assert (~ Col X A B). spliter. assumption. spliter. repeat split. intro. apply H5. unfold Out in H3. spliter. induction H10. ColR. ColR. intro. apply H6. unfold Out in H4. spliter. induction H10. ColR. ColR. ex_and H7 T. assert (I = T). { apply l6_21 with A B X Y; Col. intro; treat_equalities; Col. } subst I. exists T. split. assumption. apply bet_out_out_bet with X Y; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar