Let a be given.
Assume Ha: a ∈ S_Omega.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ {x0 ∈ S_Omega|order_rel S_Omega a x0}.
We prove the intermediate claim HxS: x ∈ S_Omega.
An exact proof term for the current goal is (SepE1 S_Omega (λx0 : set ⇒ order_rel S_Omega a x0) x Hx).
We prove the intermediate claim Hrel: order_rel S_Omega a x.
An exact proof term for the current goal is (SepE2 S_Omega (λx0 : set ⇒ order_rel S_Omega a x0) x Hx).
We prove the intermediate claim Hmem: a ∈ x.
An exact proof term for the current goal is (order_rel_well_ordered_implies_mem S_Omega a x S_Omega_well_ordered_set Hrel).
We prove the intermediate claim HrelInh: order_rel Sbar_Omega a x.
An exact proof term for the current goal is (mem_implies_order_rel_well_ordered Sbar_Omega a x Sbar_Omega_well_ordered_set Hmem).
Apply (SepI S_Omega (λx0 : set ⇒ order_rel Sbar_Omega a x0) x HxS) to the current goal.
An exact proof term for the current goal is HrelInh.
Let x be given.
Assume Hx: x ∈ {x0 ∈ S_Omega|order_rel Sbar_Omega a x0}.
We prove the intermediate claim HxS: x ∈ S_Omega.
An exact proof term for the current goal is (SepE1 S_Omega (λx0 : set ⇒ order_rel Sbar_Omega a x0) x Hx).
We prove the intermediate claim Hrel: order_rel Sbar_Omega a x.
An exact proof term for the current goal is (SepE2 S_Omega (λx0 : set ⇒ order_rel Sbar_Omega a x0) x Hx).
We prove the intermediate claim Hmem: a ∈ x.
An exact proof term for the current goal is (order_rel_well_ordered_implies_mem Sbar_Omega a x Sbar_Omega_well_ordered_set Hrel).
We prove the intermediate claim HrelSo: order_rel S_Omega a x.
An exact proof term for the current goal is (mem_implies_order_rel_well_ordered S_Omega a x S_Omega_well_ordered_set Hmem).
Apply (SepI S_Omega (λx0 : set ⇒ order_rel S_Omega a x0) x HxS) to the current goal.
An exact proof term for the current goal is HrelSo.
∎