Let x be given.
Assume Hx: x ∈ ω.
Set b to be the term open_ray_lower ω (ordsucc x).
We use b to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim Hb: ordsucc x ∈ ω.
An exact proof term for the current goal is (omega_ordsucc x Hx).
An exact proof term for the current goal is (open_ray_lower_in_order_topology_basis ω (ordsucc x) Hb).
We prove the intermediate claim Hdef: open_ray_lower ω (ordsucc x) = {y ∈ ω|order_rel ω y (ordsucc x)}.
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
Apply (SepI ω (λy : set ⇒ order_rel ω y (ordsucc x)) x Hx) to the current goal.
We prove the intermediate claim Hmem: x ∈ ordsucc x.
An exact proof term for the current goal is (ordsuccI2 x).
An exact proof term for the current goal is (mem_implies_order_rel_omega x (ordsucc x) Hmem).
∎