proposition: Lemma upper_dim_implies_not_one_side_two_sides : upper_dim_axiom -> (forall A B X Y, ~ Col X A B -> ~ Col Y A B -> ~ OS A B X Y -> TS A B X Y).
proof: Proof. intro HUD; intros. intros. induction(two_sides_dec A B X Y). assumption. apply upper_dim_implies_not_two_sides_one_side in H2; try assumption. contradiction. Qed.
imports: GeoCoq.Tarski_dev.Ch09_plane