We will prove order_topology_basis_inherited Sbar_Omega S_Omega ⊆ order_topology_basis S_Omega.

Let I be given.

Assume HI: I ∈ order_topology_basis_inherited Sbar_Omega S_Omega.

Set Ainh to be the term {I0 ∈ 𝒫 S_Omega|∃a ∈ S_Omega, ∃b ∈ S_Omega, I0 = {x ∈ S_Omega|order_rel Sbar_Omega a x ∧ order_rel Sbar_Omega x b}}.

Set Binh to be the term {I0 ∈ 𝒫 S_Omega|∃b ∈ S_Omega, I0 = {x ∈ S_Omega|order_rel Sbar_Omega x b}}.

Set Cinh to be the term {I0 ∈ 𝒫 S_Omega|∃a ∈ S_Omega, I0 = {x ∈ S_Omega|order_rel Sbar_Omega a x}}.

Set BoldInh to be the term (Ainh ∪ Binh ∪ Cinh).

We prove the intermediate claim HI0: I ∈ (BoldInh ∪ {S_Omega}).

We prove the intermediate claim Hdef: order_topology_basis_inherited Sbar_Omega S_Omega = (BoldInh ∪ {S_Omega}).

Use reflexivity.

rewrite the current goal using Hdef (from right to left).

An exact proof term for the current goal is HI.

Apply (binunionE' BoldInh {S_Omega} I (I ∈ order_topology_basis S_Omega)) to the current goal.

Assume HIBold: I ∈ BoldInh.

Apply (binunionE' (Ainh ∪ Binh) Cinh I (I ∈ order_topology_basis S_Omega)) to the current goal.

Assume HIAB: I ∈ (Ainh ∪ Binh).

Apply (binunionE' Ainh Binh I (I ∈ order_topology_basis S_Omega)) to the current goal.

Assume HIA: I ∈ Ainh.

We prove the intermediate claim Hex: ∃a ∈ S_Omega, ∃b ∈ S_Omega, I = {x ∈ S_Omega|order_rel Sbar_Omega a x ∧ order_rel Sbar_Omega x b}.

An exact proof term for the current goal is (SepE2 (𝒫 S_Omega) (λI0 : set ⇒ ∃a ∈ S_Omega, ∃b ∈ S_Omega, I0 = {x ∈ S_Omega|order_rel Sbar_Omega a x ∧ order_rel Sbar_Omega x b}) I HIA).

Apply Hex to the current goal.

Let a be given.

Assume HaPair.

Apply HaPair to the current goal.

Assume HaS: a ∈ S_Omega.

Assume Hexb.

Apply Hexb to the current goal.

Let b be given.

Assume HbPair.

Apply HbPair to the current goal.

Assume HbS: b ∈ S_Omega.

Assume HIeq: I = {x ∈ S_Omega|order_rel Sbar_Omega a x ∧ order_rel Sbar_Omega x b}.

We prove the intermediate claim HIeq2: I = {x ∈ S_Omega|order_rel S_Omega a x ∧ order_rel S_Omega x b}.

rewrite the current goal using HIeq (from left to right).

rewrite the current goal using (SOmega_interval_eq_inherited a b HaS HbS) (from right to left).

Use reflexivity.

We will prove I ∈ order_topology_basis S_Omega.

Set S1 to be the term {I0 ∈ 𝒫 S_Omega|∃a0 ∈ S_Omega, ∃b0 ∈ S_Omega, I0 = {x ∈ S_Omega|order_rel S_Omega a0 x ∧ order_rel S_Omega x b0}}.

Set S2 to be the term {I0 ∈ 𝒫 S_Omega|∃b0 ∈ S_Omega, I0 = {x ∈ S_Omega|order_rel S_Omega x b0}}.

Set S3 to be the term {I0 ∈ 𝒫 S_Omega|∃a0 ∈ S_Omega, I0 = {x ∈ S_Omega|order_rel S_Omega a0 x}}.

Set Bold0 to be the term (S1 ∪ S2 ∪ S3).

We prove the intermediate claim Hdef: order_topology_basis S_Omega = (Bold0 ∪ {S_Omega}).

Use reflexivity.

rewrite the current goal using Hdef (from left to right).

Apply binunionI1 to the current goal.

We will prove I ∈ {I0 ∈ 𝒫 S_Omega|∃a0 ∈ S_Omega, ∃b0 ∈ S_Omega, I0 = {x ∈ S_Omega|order_rel S_Omega a0 x ∧ order_rel S_Omega x b0}}.

We prove the intermediate claim HIPow: I ∈ 𝒫 S_Omega.

Apply PowerI S_Omega I to the current goal.

Let x be given.

Assume Hx: x ∈ I.

We prove the intermediate claim Hx': x ∈ {x0 ∈ S_Omega|order_rel S_Omega a x0 ∧ order_rel S_Omega x0 b}.

rewrite the current goal using HIeq2 (from right to left).

An exact proof term for the current goal is Hx.

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 HIprop: ∃a0 ∈ S_Omega, ∃b0 ∈ S_Omega, I = {x ∈ S_Omega|order_rel S_Omega a0 x ∧ order_rel S_Omega x b0}.

We use a to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HaS.

We use b to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HbS.

An exact proof term for the current goal is HIeq2.

An exact proof term for the current goal is (SepI (𝒫 S_Omega) (λI0 : set ⇒ ∃a0 ∈ S_Omega, ∃b0 ∈ S_Omega, I0 = {x ∈ S_Omega|order_rel S_Omega a0 x ∧ order_rel S_Omega x b0}) I HIPow HIprop).

Assume HIB: I ∈ Binh.

We prove the intermediate claim Hex: ∃b ∈ S_Omega, I = {x ∈ S_Omega|order_rel Sbar_Omega x b}.

An exact proof term for the current goal is (SepE2 (𝒫 S_Omega) (λI0 : set ⇒ ∃b ∈ S_Omega, I0 = {x ∈ S_Omega|order_rel Sbar_Omega x b}) I HIB).

Apply Hex to the current goal.

Let b be given.

Assume HbPair.

Apply HbPair to the current goal.

Assume HbS: b ∈ S_Omega.

Assume HIeq: I = {x ∈ S_Omega|order_rel Sbar_Omega x b}.

We prove the intermediate claim HIeq2: I = {x ∈ S_Omega|order_rel S_Omega x b}.

rewrite the current goal using HIeq (from left to right).

rewrite the current goal using (SOmega_left_ray_eq_inherited b HbS) (from right to left).

Use reflexivity.

We will prove I ∈ order_topology_basis S_Omega.

Set S1 to be the term {I0 ∈ 𝒫 S_Omega|∃a0 ∈ S_Omega, ∃b0 ∈ S_Omega, I0 = {x ∈ S_Omega|order_rel S_Omega a0 x ∧ order_rel S_Omega x b0}}.

Set S2 to be the term {I0 ∈ 𝒫 S_Omega|∃b0 ∈ S_Omega, I0 = {x ∈ S_Omega|order_rel S_Omega x b0}}.

Set S3 to be the term {I0 ∈ 𝒫 S_Omega|∃a0 ∈ S_Omega, I0 = {x ∈ S_Omega|order_rel S_Omega a0 x}}.

Set Bold0 to be the term (S1 ∪ S2 ∪ S3).

We prove the intermediate claim Hdef: order_topology_basis S_Omega = (Bold0 ∪ {S_Omega}).

Use reflexivity.

rewrite the current goal using Hdef (from left to right).

Apply binunionI1 to the current goal.

Apply binunionI2 to the current goal.

We will prove I ∈ {I0 ∈ 𝒫 S_Omega|∃b0 ∈ S_Omega, I0 = {x ∈ S_Omega|order_rel S_Omega x b0}}.

We prove the intermediate claim HIPow: I ∈ 𝒫 S_Omega.

Apply PowerI S_Omega I to the current goal.

Let x be given.

Assume Hx: x ∈ I.

We prove the intermediate claim Hx': x ∈ {x0 ∈ S_Omega|order_rel S_Omega x0 b}.

rewrite the current goal using HIeq2 (from right to left).

An exact proof term for the current goal is Hx.

An exact proof term for the current goal is (SepE1 S_Omega (λx0 : set ⇒ order_rel S_Omega x0 b) x Hx').

We prove the intermediate claim HIprop: ∃b0 ∈ S_Omega, I = {x ∈ S_Omega|order_rel S_Omega x b0}.

We use b to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HbS.

An exact proof term for the current goal is HIeq2.

An exact proof term for the current goal is (SepI (𝒫 S_Omega) (λI0 : set ⇒ ∃b0 ∈ S_Omega, I0 = {x ∈ S_Omega|order_rel S_Omega x b0}) I HIPow HIprop).

An exact proof term for the current goal is HIAB.

Assume HIC: I ∈ Cinh.

We prove the intermediate claim Hex: ∃a ∈ S_Omega, I = {x ∈ S_Omega|order_rel Sbar_Omega a x}.

An exact proof term for the current goal is (SepE2 (𝒫 S_Omega) (λI0 : set ⇒ ∃a ∈ S_Omega, I0 = {x ∈ S_Omega|order_rel Sbar_Omega a x}) I HIC).

Apply Hex to the current goal.

Let a be given.

Assume HaPair.

Apply HaPair to the current goal.

Assume HaS: a ∈ S_Omega.

Assume HIeq: I = {x ∈ S_Omega|order_rel Sbar_Omega a x}.

We prove the intermediate claim HIeq2: I = {x ∈ S_Omega|order_rel S_Omega a x}.

rewrite the current goal using HIeq (from left to right).

rewrite the current goal using (SOmega_right_ray_eq_inherited a HaS) (from right to left).

Use reflexivity.

We will prove I ∈ order_topology_basis S_Omega.

Set S1 to be the term {I0 ∈ 𝒫 S_Omega|∃a0 ∈ S_Omega, ∃b0 ∈ S_Omega, I0 = {x ∈ S_Omega|order_rel S_Omega a0 x ∧ order_rel S_Omega x b0}}.

Set S2 to be the term {I0 ∈ 𝒫 S_Omega|∃b0 ∈ S_Omega, I0 = {x ∈ S_Omega|order_rel S_Omega x b0}}.

Set S3 to be the term {I0 ∈ 𝒫 S_Omega|∃a0 ∈ S_Omega, I0 = {x ∈ S_Omega|order_rel S_Omega a0 x}}.

Set Bold0 to be the term (S1 ∪ S2 ∪ S3).

We prove the intermediate claim Hdef: order_topology_basis S_Omega = (Bold0 ∪ {S_Omega}).

Use reflexivity.

rewrite the current goal using Hdef (from left to right).

Apply binunionI1 to the current goal.

Apply binunionI2 to the current goal.

We will prove I ∈ {I0 ∈ 𝒫 S_Omega|∃a0 ∈ S_Omega, I0 = {x ∈ S_Omega|order_rel S_Omega a0 x}}.

We prove the intermediate claim HIPow: I ∈ 𝒫 S_Omega.

Apply PowerI S_Omega I to the current goal.

Let x be given.

Assume Hx: x ∈ I.

We prove the intermediate claim Hx': x ∈ {x0 ∈ S_Omega|order_rel S_Omega a x0}.

rewrite the current goal using HIeq2 (from right to left).

An exact proof term for the current goal is Hx.

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 HIprop: ∃a0 ∈ S_Omega, I = {x ∈ S_Omega|order_rel S_Omega a0 x}.

We use a to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HaS.

An exact proof term for the current goal is HIeq2.

An exact proof term for the current goal is (SepI (𝒫 S_Omega) (λI0 : set ⇒ ∃a0 ∈ S_Omega, I0 = {x ∈ S_Omega|order_rel S_Omega a0 x}) I HIPow HIprop).

We will prove I ∈ (Ainh ∪ Binh) ∪ Cinh.

We prove the intermediate claim HdefBold: BoldInh = (Ainh ∪ Binh) ∪ Cinh.

Use reflexivity.

rewrite the current goal using HdefBold (from right to left).

An exact proof term for the current goal is HIBold.

Assume HIwhole: I ∈ {S_Omega}.

We will prove I ∈ order_topology_basis S_Omega.

Set S1 to be the term {I0 ∈ 𝒫 S_Omega|∃a0 ∈ S_Omega, ∃b0 ∈ S_Omega, I0 = {x ∈ S_Omega|order_rel S_Omega a0 x ∧ order_rel S_Omega x b0}}.

Set S2 to be the term {I0 ∈ 𝒫 S_Omega|∃b0 ∈ S_Omega, I0 = {x ∈ S_Omega|order_rel S_Omega x b0}}.

Set S3 to be the term {I0 ∈ 𝒫 S_Omega|∃a0 ∈ S_Omega, I0 = {x ∈ S_Omega|order_rel S_Omega a0 x}}.

Set Bold0 to be the term (S1 ∪ S2 ∪ S3).

We prove the intermediate claim Hdef: order_topology_basis S_Omega = (Bold0 ∪ {S_Omega}).

Use reflexivity.

rewrite the current goal using Hdef (from left to right).

Apply binunionI2 to the current goal.

An exact proof term for the current goal is HIwhole.

An exact proof term for the current goal is HI0.

We will prove order_topology_basis S_Omega ⊆ order_topology_basis_inherited Sbar_Omega S_Omega.

Let I be given.

Assume HI: I ∈ order_topology_basis S_Omega.

Set A0 to be the term {I0 ∈ 𝒫 S_Omega|∃a ∈ S_Omega, ∃b ∈ S_Omega, I0 = {x ∈ S_Omega|order_rel S_Omega a x ∧ order_rel S_Omega x b}}.

Set B0 to be the term {I0 ∈ 𝒫 S_Omega|∃b ∈ S_Omega, I0 = {x ∈ S_Omega|order_rel S_Omega x b}}.

Set C0 to be the term {I0 ∈ 𝒫 S_Omega|∃a ∈ S_Omega, I0 = {x ∈ S_Omega|order_rel S_Omega a x}}.

Set Bold0 to be the term (A0 ∪ B0 ∪ C0).

We prove the intermediate claim HI0: I ∈ (Bold0 ∪ {S_Omega}).

We prove the intermediate claim Hdef: order_topology_basis S_Omega = (Bold0 ∪ {S_Omega}).

Use reflexivity.

rewrite the current goal using Hdef (from right to left).

An exact proof term for the current goal is HI.

Apply (binunionE' Bold0 {S_Omega} I (I ∈ order_topology_basis_inherited Sbar_Omega S_Omega)) to the current goal.

Assume HIBold: I ∈ Bold0.

Apply (binunionE' (A0 ∪ B0) C0 I (I ∈ order_topology_basis_inherited Sbar_Omega S_Omega)) to the current goal.

Assume HIAB: I ∈ (A0 ∪ B0).

Apply (binunionE' A0 B0 I (I ∈ order_topology_basis_inherited Sbar_Omega S_Omega)) to the current goal.

Assume HIA: I ∈ A0.

We prove the intermediate claim Hex: ∃a ∈ S_Omega, ∃b ∈ S_Omega, I = {x ∈ S_Omega|order_rel S_Omega a x ∧ order_rel S_Omega x b}.

An exact proof term for the current goal is (SepE2 (𝒫 S_Omega) (λI0 : set ⇒ ∃a ∈ S_Omega, ∃b ∈ S_Omega, I0 = {x ∈ S_Omega|order_rel S_Omega a x ∧ order_rel S_Omega x b}) I HIA).

Apply Hex to the current goal.

Let a be given.

Assume HaPair.

Apply HaPair to the current goal.

Assume HaS: a ∈ S_Omega.

Assume Hexb.

Apply Hexb to the current goal.

Let b be given.

Assume HbPair.

Apply HbPair to the current goal.

Assume HbS: b ∈ S_Omega.

Assume HIeq: I = {x ∈ S_Omega|order_rel S_Omega a x ∧ order_rel S_Omega x b}.

We prove the intermediate claim HIeq2: I = {x ∈ S_Omega|order_rel Sbar_Omega a x ∧ order_rel Sbar_Omega x b}.

rewrite the current goal using HIeq (from left to right).

rewrite the current goal using (SOmega_interval_eq_inherited a b HaS HbS) (from left to right).

Use reflexivity.

We will prove I ∈ order_topology_basis_inherited Sbar_Omega S_Omega.

Set Ainh to be the term {I0 ∈ 𝒫 S_Omega|∃a0 ∈ S_Omega, ∃b0 ∈ S_Omega, I0 = {x ∈ S_Omega|order_rel Sbar_Omega a0 x ∧ order_rel Sbar_Omega x b0}}.

Set Binh to be the term {I0 ∈ 𝒫 S_Omega|∃b0 ∈ S_Omega, I0 = {x ∈ S_Omega|order_rel Sbar_Omega x b0}}.

Set Cinh to be the term {I0 ∈ 𝒫 S_Omega|∃a0 ∈ S_Omega, I0 = {x ∈ S_Omega|order_rel Sbar_Omega a0 x}}.

Set BoldInh to be the term (Ainh ∪ Binh ∪ Cinh).

We prove the intermediate claim Hdef: order_topology_basis_inherited Sbar_Omega S_Omega = (BoldInh ∪ {S_Omega}).

Use reflexivity.

rewrite the current goal using Hdef (from left to right).

Apply binunionI1 to the current goal.

We will prove I ∈ {I0 ∈ 𝒫 S_Omega|∃a0 ∈ S_Omega, ∃b0 ∈ S_Omega, I0 = {x ∈ S_Omega|order_rel Sbar_Omega a0 x ∧ order_rel Sbar_Omega x b0}}.

We prove the intermediate claim HIPow: I ∈ 𝒫 S_Omega.

Apply PowerI S_Omega I to the current goal.

Let x be given.

Assume Hx: x ∈ I.

We prove the intermediate claim Hx': x ∈ {x0 ∈ S_Omega|order_rel Sbar_Omega a x0 ∧ order_rel Sbar_Omega x0 b}.

rewrite the current goal using HIeq2 (from right to left).

An exact proof term for the current goal is Hx.

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 HIprop: ∃a0 ∈ S_Omega, ∃b0 ∈ S_Omega, I = {x ∈ S_Omega|order_rel Sbar_Omega a0 x ∧ order_rel Sbar_Omega x b0}.

We use a to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HaS.

We use b to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HbS.

An exact proof term for the current goal is HIeq2.

An exact proof term for the current goal is (SepI (𝒫 S_Omega) (λI0 : set ⇒ ∃a0 ∈ S_Omega, ∃b0 ∈ S_Omega, I0 = {x ∈ S_Omega|order_rel Sbar_Omega a0 x ∧ order_rel Sbar_Omega x b0}) I HIPow HIprop).

Assume HIB: I ∈ B0.

We prove the intermediate claim Hex: ∃b ∈ S_Omega, I = {x ∈ S_Omega|order_rel S_Omega x b}.

An exact proof term for the current goal is (SepE2 (𝒫 S_Omega) (λI0 : set ⇒ ∃b ∈ S_Omega, I0 = {x ∈ S_Omega|order_rel S_Omega x b}) I HIB).

Apply Hex to the current goal.

Let b be given.

Assume HbPair.

Apply HbPair to the current goal.

Assume HbS: b ∈ S_Omega.

Assume HIeq: I = {x ∈ S_Omega|order_rel S_Omega x b}.

We prove the intermediate claim HIeq2: I = {x ∈ S_Omega|order_rel Sbar_Omega x b}.

rewrite the current goal using HIeq (from left to right).

rewrite the current goal using (SOmega_left_ray_eq_inherited b HbS) (from left to right).

Use reflexivity.

We will prove I ∈ order_topology_basis_inherited Sbar_Omega S_Omega.

Set Ainh to be the term {I0 ∈ 𝒫 S_Omega|∃a0 ∈ S_Omega, ∃b0 ∈ S_Omega, I0 = {x ∈ S_Omega|order_rel Sbar_Omega a0 x ∧ order_rel Sbar_Omega x b0}}.

Set Binh to be the term {I0 ∈ 𝒫 S_Omega|∃b0 ∈ S_Omega, I0 = {x ∈ S_Omega|order_rel Sbar_Omega x b0}}.

Set Cinh to be the term {I0 ∈ 𝒫 S_Omega|∃a0 ∈ S_Omega, I0 = {x ∈ S_Omega|order_rel Sbar_Omega a0 x}}.

Set BoldInh to be the term (Ainh ∪ Binh ∪ Cinh).

We prove the intermediate claim Hdef: order_topology_basis_inherited Sbar_Omega S_Omega = (BoldInh ∪ {S_Omega}).

Use reflexivity.

rewrite the current goal using Hdef (from left to right).

Apply binunionI1 to the current goal.

Apply binunionI2 to the current goal.

We will prove I ∈ {I0 ∈ 𝒫 S_Omega|∃b0 ∈ S_Omega, I0 = {x ∈ S_Omega|order_rel Sbar_Omega x b0}}.

We prove the intermediate claim HIPow: I ∈ 𝒫 S_Omega.

Apply PowerI S_Omega I to the current goal.

Let x be given.

Assume Hx: x ∈ I.

We prove the intermediate claim Hx': x ∈ {x0 ∈ S_Omega|order_rel Sbar_Omega x0 b}.

rewrite the current goal using HIeq2 (from right to left).

An exact proof term for the current goal is Hx.

An exact proof term for the current goal is (SepE1 S_Omega (λx0 : set ⇒ order_rel Sbar_Omega x0 b) x Hx').

We prove the intermediate claim HIprop: ∃b0 ∈ S_Omega, I = {x ∈ S_Omega|order_rel Sbar_Omega x b0}.

We use b to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HbS.

An exact proof term for the current goal is HIeq2.

An exact proof term for the current goal is (SepI (𝒫 S_Omega) (λI0 : set ⇒ ∃b0 ∈ S_Omega, I0 = {x ∈ S_Omega|order_rel Sbar_Omega x b0}) I HIPow HIprop).

An exact proof term for the current goal is HIAB.

Assume HIC: I ∈ C0.

We prove the intermediate claim Hex: ∃a ∈ S_Omega, I = {x ∈ S_Omega|order_rel S_Omega a x}.

An exact proof term for the current goal is (SepE2 (𝒫 S_Omega) (λI0 : set ⇒ ∃a ∈ S_Omega, I0 = {x ∈ S_Omega|order_rel S_Omega a x}) I HIC).

Apply Hex to the current goal.

Let a be given.

Assume HaPair.

Apply HaPair to the current goal.

Assume HaS: a ∈ S_Omega.

Assume HIeq: I = {x ∈ S_Omega|order_rel S_Omega a x}.

We prove the intermediate claim HIeq2: I = {x ∈ S_Omega|order_rel Sbar_Omega a x}.

rewrite the current goal using HIeq (from left to right).

rewrite the current goal using (SOmega_right_ray_eq_inherited a HaS) (from left to right).

Use reflexivity.

We will prove I ∈ order_topology_basis_inherited Sbar_Omega S_Omega.

Set Ainh to be the term {I0 ∈ 𝒫 S_Omega|∃a0 ∈ S_Omega, ∃b0 ∈ S_Omega, I0 = {x ∈ S_Omega|order_rel Sbar_Omega a0 x ∧ order_rel Sbar_Omega x b0}}.

Set Binh to be the term {I0 ∈ 𝒫 S_Omega|∃b0 ∈ S_Omega, I0 = {x ∈ S_Omega|order_rel Sbar_Omega x b0}}.

Set Cinh to be the term {I0 ∈ 𝒫 S_Omega|∃a0 ∈ S_Omega, I0 = {x ∈ S_Omega|order_rel Sbar_Omega a0 x}}.

Set BoldInh to be the term (Ainh ∪ Binh ∪ Cinh).

We prove the intermediate claim Hdef: order_topology_basis_inherited Sbar_Omega S_Omega = (BoldInh ∪ {S_Omega}).

Use reflexivity.

rewrite the current goal using Hdef (from left to right).

Apply binunionI1 to the current goal.

Apply binunionI2 to the current goal.

We will prove I ∈ {I0 ∈ 𝒫 S_Omega|∃a0 ∈ S_Omega, I0 = {x ∈ S_Omega|order_rel Sbar_Omega a0 x}}.

We prove the intermediate claim HIPow: I ∈ 𝒫 S_Omega.

Apply PowerI S_Omega I to the current goal.

Let x be given.

Assume Hx: x ∈ I.

We prove the intermediate claim Hx': x ∈ {x0 ∈ S_Omega|order_rel Sbar_Omega a x0}.

rewrite the current goal using HIeq2 (from right to left).

An exact proof term for the current goal is Hx.

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 HIprop: ∃a0 ∈ S_Omega, I = {x ∈ S_Omega|order_rel Sbar_Omega a0 x}.

We use a to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HaS.

An exact proof term for the current goal is HIeq2.

An exact proof term for the current goal is (SepI (𝒫 S_Omega) (λI0 : set ⇒ ∃a0 ∈ S_Omega, I0 = {x ∈ S_Omega|order_rel Sbar_Omega a0 x}) I HIPow HIprop).

We will prove I ∈ (A0 ∪ B0) ∪ C0.

We prove the intermediate claim HdefBold: Bold0 = (A0 ∪ B0) ∪ C0.

Use reflexivity.

rewrite the current goal using HdefBold (from right to left).

An exact proof term for the current goal is HIBold.

Assume HIwhole: I ∈ {S_Omega}.

We will prove I ∈ order_topology_basis_inherited Sbar_Omega S_Omega.

Set Ainh to be the term {I0 ∈ 𝒫 S_Omega|∃a0 ∈ S_Omega, ∃b0 ∈ S_Omega, I0 = {x ∈ S_Omega|order_rel Sbar_Omega a0 x ∧ order_rel Sbar_Omega x b0}}.

Set Binh to be the term {I0 ∈ 𝒫 S_Omega|∃b0 ∈ S_Omega, I0 = {x ∈ S_Omega|order_rel Sbar_Omega x b0}}.

Set Cinh to be the term {I0 ∈ 𝒫 S_Omega|∃a0 ∈ S_Omega, I0 = {x ∈ S_Omega|order_rel Sbar_Omega a0 x}}.

Set BoldInh to be the term (Ainh ∪ Binh ∪ Cinh).

We prove the intermediate claim Hdef: order_topology_basis_inherited Sbar_Omega S_Omega = (BoldInh ∪ {S_Omega}).

Use reflexivity.

rewrite the current goal using Hdef (from left to right).

Apply binunionI2 to the current goal.

An exact proof term for the current goal is HIwhole.

An exact proof term for the current goal is HI0.