Let X be given.
Assume Hwo: well_ordered_set X.
Assume H1X: 1 ∈ X.
Apply set_ext to the current goal.
Let y be given.
Assume Hy: y ∈ open_ray_lower X 1.
We will prove y ∈ {0}.
We prove the intermediate claim Hyrel: order_rel X y 1.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X x0 1) y Hy).
We prove the intermediate claim Hy1: y ∈ 1.
An exact proof term for the current goal is (order_rel_well_ordered_implies_mem X y 1 Hwo Hyrel).
rewrite the current goal using (eq_1_Sing0) (from right to left).
An exact proof term for the current goal is Hy1.
Let y be given.
Assume Hy0: y ∈ {0}.
We will prove y ∈ open_ray_lower X 1.
We prove the intermediate claim Hyeq: y = 0.
An exact proof term for the current goal is (SingE 0 y Hy0).
rewrite the current goal using Hyeq (from left to right).
We prove the intermediate claim HordX: ordinal X.
An exact proof term for the current goal is (well_ordered_set_is_ordinal X Hwo).
We prove the intermediate claim HtransX: TransSet X.
An exact proof term for the current goal is (andEL (TransSet X) (∀beta ∈ X, TransSet beta) HordX).
We prove the intermediate claim H0X: 0 ∈ X.
We prove the intermediate claim H0in1: 0 ∈ 1.
rewrite the current goal using (eq_1_Sing0) (from left to right).
An exact proof term for the current goal is (SingI 0).
We prove the intermediate claim H1subX: 1 ⊆ X.
An exact proof term for the current goal is (HtransX 1 H1X).
An exact proof term for the current goal is (H1subX 0 H0in1).
We prove the intermediate claim H01: 0 ∈ 1.
rewrite the current goal using (eq_1_Sing0) (from left to right).
An exact proof term for the current goal is (SingI 0).
We prove the intermediate claim Hrel01: order_rel X 0 1.
An exact proof term for the current goal is (mem_implies_order_rel_well_ordered X 0 1 Hwo H01).
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ order_rel X x0 1) 0 H0X Hrel01).
∎