We will prove convex_in Sbar_Omega S_Omega.
We will prove S_Omega ⊆ Sbar_Omega ∧ ∀a b : set, a ∈ S_Omega → b ∈ S_Omega → order_interval Sbar_Omega a b ⊆ S_Omega.
Apply andI to the current goal.
An exact proof term for the current goal is S_Omega_Subq_Sbar_Omega.
Let a and b be given.
Assume Ha: a ∈ S_Omega.
Assume Hb: b ∈ S_Omega.
We will prove order_interval Sbar_Omega a b ⊆ S_Omega.
Let x be given.
Assume HxInt: x ∈ order_interval Sbar_Omega a b.
We will prove x ∈ S_Omega.
We prove the intermediate claim Hpack: x ∈ Sbar_Omega ∧ (order_rel Sbar_Omega a x ∧ order_rel Sbar_Omega x b).
An exact proof term for the current goal is (order_intervalE Sbar_Omega a b x HxInt).
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 (andER (x ∈ Sbar_Omega) (order_rel Sbar_Omega a x ∧ order_rel Sbar_Omega x b) Hpack).
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 HxInb: 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 HbSub: b ⊆ S_Omega.
An exact proof term for the current goal is (S_Omega_TransSet b Hb).
An exact proof term for the current goal is (HbSub x HxInb).
∎