We will prove ∃X Y : set, convex_in X Y ∧ Y ≠ X ∧ ¬ interval_or_ray_in X Y.
We use rational_numbers to witness the existential quantifier.
We use Q_sqrt2_cut to witness the existential quantifier.
We will prove convex_in rational_numbers Q_sqrt2_cut ∧ Q_sqrt2_cut ≠ rational_numbers ∧ ¬ interval_or_ray_in rational_numbers Q_sqrt2_cut.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Q_sqrt2_cut_convex.
An exact proof term for the current goal is Q_sqrt2_cut_neq_Q.
An exact proof term for the current goal is Q_sqrt2_cut_not_interval_or_ray.
∎