Let a and b be given.
Assume Ha: a ∈ S_Omega.
Assume Hb: b ∈ S_Omega.
Apply set_ext to the current goal.
We will prove {x ∈ S_Omega|order_rel S_Omega a x ∧ order_rel S_Omega x b} ⊆ {x ∈ S_Omega|order_rel Sbar_Omega a x ∧ order_rel Sbar_Omega x b}.
Let x be given.
Assume Hx: x ∈ {x0 ∈ S_Omega|order_rel S_Omega a x0 ∧ order_rel S_Omega x0 b}.
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 ∧ order_rel S_Omega x0 b) x Hx).
We prove the intermediate claim Hrel: order_rel S_Omega a x ∧ order_rel S_Omega x b.
An exact proof term for the current goal is (SepE2 S_Omega (λx0 : set ⇒ order_rel S_Omega a x0 ∧ order_rel S_Omega x0 b) x Hx).
We prove the intermediate claim Hax: order_rel S_Omega a x.
An exact proof term for the current goal is (andEL (order_rel S_Omega a x) (order_rel S_Omega x b) Hrel).
We prove the intermediate claim Hxb: order_rel S_Omega x b.
An exact proof term for the current goal is (andER (order_rel S_Omega a x) (order_rel S_Omega x b) Hrel).
We prove the intermediate claim Hamem: 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 Hax).
We prove the intermediate claim Hxmem: x ∈ b.
An exact proof term for the current goal is (order_rel_well_ordered_implies_mem S_Omega x b S_Omega_well_ordered_set Hxb).
We prove the intermediate claim HaxInh: 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 Hamem).
We prove the intermediate claim HxbInh: order_rel Sbar_Omega x b.
An exact proof term for the current goal is (mem_implies_order_rel_well_ordered Sbar_Omega x b Sbar_Omega_well_ordered_set Hxmem).
Apply (SepI S_Omega (λx0 : set ⇒ order_rel Sbar_Omega a x0 ∧ order_rel Sbar_Omega x0 b) x HxS) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HaxInh.
An exact proof term for the current goal is HxbInh.
We will prove {x ∈ S_Omega|order_rel Sbar_Omega a x ∧ order_rel Sbar_Omega x b} ⊆ {x ∈ S_Omega|order_rel S_Omega a x ∧ order_rel S_Omega x b}.
Let x be given.
Assume Hx: x ∈ {x0 ∈ S_Omega|order_rel Sbar_Omega a x0 ∧ order_rel Sbar_Omega x0 b}.
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 ∧ order_rel Sbar_Omega x0 b) x Hx).
We prove the intermediate claim Hrel: order_rel Sbar_Omega a x ∧ order_rel Sbar_Omega x b.
An exact proof term for the current goal is (SepE2 S_Omega (λx0 : set ⇒ order_rel Sbar_Omega a x0 ∧ order_rel Sbar_Omega x0 b) x Hx).
We prove the intermediate claim Hax: order_rel Sbar_Omega a x.
An exact proof term for the current goal is (andEL (order_rel Sbar_Omega a x) (order_rel Sbar_Omega x b) Hrel).
We prove the intermediate claim Hxb: order_rel Sbar_Omega x b.
An exact proof term for the current goal is (andER (order_rel Sbar_Omega a x) (order_rel Sbar_Omega x b) Hrel).
We prove the intermediate claim Hamem: 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 Hax).
We prove the intermediate claim Hxmem: x ∈ b.
An exact proof term for the current goal is (order_rel_well_ordered_implies_mem Sbar_Omega x b Sbar_Omega_well_ordered_set Hxb).
We prove the intermediate claim HaxSo: 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 Hamem).
We prove the intermediate claim HxbSo: order_rel S_Omega x b.
An exact proof term for the current goal is (mem_implies_order_rel_well_ordered S_Omega x b S_Omega_well_ordered_set Hxmem).
Apply (SepI S_Omega (λx0 : set ⇒ order_rel S_Omega a x0 ∧ order_rel S_Omega x0 b) x HxS) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HaxSo.
An exact proof term for the current goal is HxbSo.
∎