Let a be given.

Assume HaA: a ∈ A.

We will prove a ∈ U.

We prove the intermediate claim HaX: a ∈ X.

An exact proof term for the current goal is (HAsubX a HaA).

We prove the intermediate claim Ha0': ¬ (a = 0).

Assume HaEq0: a = 0.

We prove the intermediate claim H0A: 0 ∈ A.

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

An exact proof term for the current goal is HaA.

An exact proof term for the current goal is (H0An H0A).

We prove the intermediate claim Hexb: ∃b ∈ order_topology_basis X, a ∈ b ∧ b ⊆ UB.

An exact proof term for the current goal is (HexA_basis a HaA).

Apply Hexb to the current goal.

Let b be given.

Assume HbCore.

Apply HbCore to the current goal.

Assume HbB HbData.

Apply HbData to the current goal.

Assume Hab HbsubUB.

We prove the intermediate claim Hexx: ∃x ∈ X, order_rel X x a ∧ order_interval_right_closed X x a ⊆ b.

An exact proof term for the current goal is (order_topology_basis_contains_right_closed_interval X b a Hwo Hso HaX Ha0' HbB Hab).

Apply Hexx to the current goal.

Let x be given.

Assume HxCore.

Apply HxCore to the current goal.

Assume HxX HxData.

Apply HxData to the current goal.

Assume Hxa HIsubb.

We prove the intermediate claim HaI: a ∈ order_interval_right_closed X x a.

We prove the intermediate claim HIdef: order_interval_right_closed X x a = {z ∈ X|order_rel X x z ∧ (z = a ∨ order_rel X z a)}.

Use reflexivity.

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

Apply (SepI X (λz0 : set ⇒ order_rel X x z0 ∧ (z0 = a ∨ order_rel X z0 a)) a HaX) to the current goal.

Apply andI to the current goal.

An exact proof term for the current goal is Hxa.

Apply orIL to the current goal.

Use reflexivity.

We prove the intermediate claim HIopen: order_interval_right_closed X x a ∈ order_topology X.

An exact proof term for the current goal is (order_interval_right_closed_open X x a Hwo Hso HxX HaX Hxa).

We prove the intermediate claim HIsubUB: order_interval_right_closed X x a ⊆ UB.

Let z be given.

Assume HzI: z ∈ order_interval_right_closed X x a.

We will prove z ∈ UB.

We prove the intermediate claim Hzb: z ∈ b.

An exact proof term for the current goal is (HIsubb z HzI).

An exact proof term for the current goal is (HbsubUB z Hzb).

We prove the intermediate claim HIinFamA: order_interval_right_closed X x a ∈ FamA.

Apply (SepI (order_topology X) (λI0 : set ⇒ ∃a0 ∈ A, ∃x0 ∈ X, order_rel X x0 a0 ∧ I0 = order_interval_right_closed X x0 a0 ∧ order_interval_right_closed X x0 a0 ⊆ UB) (order_interval_right_closed X x a) HIopen) to the current goal.

We use a to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HaA.

We use x to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HxX.

Apply andI to the current goal.

An exact proof term for the current goal is Hxa.

Use reflexivity.

An exact proof term for the current goal is HIsubUB.

An exact proof term for the current goal is (UnionI FamA a (order_interval_right_closed X x a) HaI HIinFamA).

Let b be given.

Assume HbB: b ∈ B.

We will prove b ∈ V.

We prove the intermediate claim HbX: b ∈ X.

An exact proof term for the current goal is (HBsubX b HbB).

We prove the intermediate claim Hb0': ¬ (b = 0).

Assume HbEq0: b = 0.

We prove the intermediate claim H0B: 0 ∈ B.

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

An exact proof term for the current goal is HbB.

An exact proof term for the current goal is (H0Bn H0B).

We prove the intermediate claim Hexc: ∃c ∈ order_topology_basis X, b ∈ c ∧ c ⊆ VA.

An exact proof term for the current goal is (HexB_basis b HbB).

Apply Hexc to the current goal.

Let c be given.

Assume HcCore.

Apply HcCore to the current goal.

Assume HcB HcData.

Apply HcData to the current goal.

Assume Hbc HcsubVA.

We prove the intermediate claim Hexy: ∃y ∈ X, order_rel X y b ∧ order_interval_right_closed X y b ⊆ c.

An exact proof term for the current goal is (order_topology_basis_contains_right_closed_interval X c b Hwo Hso HbX Hb0' HcB Hbc).

Apply Hexy to the current goal.

Let y be given.

Assume HyCore.

Apply HyCore to the current goal.

Assume HyX HyData.

Apply HyData to the current goal.

Assume Hyb HJsubc.

We prove the intermediate claim HbJ: b ∈ order_interval_right_closed X y b.

We prove the intermediate claim HJdef: order_interval_right_closed X y b = {z ∈ X|order_rel X y z ∧ (z = b ∨ order_rel X z b)}.

Use reflexivity.

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

Apply (SepI X (λz0 : set ⇒ order_rel X y z0 ∧ (z0 = b ∨ order_rel X z0 b)) b HbX) to the current goal.

Apply andI to the current goal.

An exact proof term for the current goal is Hyb.

Apply orIL to the current goal.

Use reflexivity.

We prove the intermediate claim HJopen: order_interval_right_closed X y b ∈ order_topology X.

An exact proof term for the current goal is (order_interval_right_closed_open X y b Hwo Hso HyX HbX Hyb).

We prove the intermediate claim HJsubVA: order_interval_right_closed X y b ⊆ VA.

Let z be given.

Assume HzJ: z ∈ order_interval_right_closed X y b.

We will prove z ∈ VA.

We prove the intermediate claim Hzc: z ∈ c.

An exact proof term for the current goal is (HJsubc z HzJ).

An exact proof term for the current goal is (HcsubVA z Hzc).

We prove the intermediate claim HJinFamB: order_interval_right_closed X y b ∈ FamB.

Apply (SepI (order_topology X) (λJ0 : set ⇒ ∃b0 ∈ B, ∃y0 ∈ X, order_rel X y0 b0 ∧ J0 = order_interval_right_closed X y0 b0 ∧ order_interval_right_closed X y0 b0 ⊆ VA) (order_interval_right_closed X y b) HJopen) to the current goal.

We use b to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HbB.

We use y to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HyX.

Apply andI to the current goal.

An exact proof term for the current goal is Hyb.

Use reflexivity.

An exact proof term for the current goal is HJsubVA.

An exact proof term for the current goal is (UnionI FamB b (order_interval_right_closed X y b) HbJ HJinFamB).

Apply Empty_eq to the current goal.

Let z be given.

Assume HzUV: z ∈ U ∩ V.

We will prove False.

We prove the intermediate claim HzU: z ∈ U.

An exact proof term for the current goal is (binintersectE1 U V z HzUV).

We prove the intermediate claim HzV: z ∈ V.

An exact proof term for the current goal is (binintersectE2 U V z HzUV).

We prove the intermediate claim HUdef: U = ⋃ FamA.

Use reflexivity.

We prove the intermediate claim HVdef: V = ⋃ FamB.

Use reflexivity.

We prove the intermediate claim HzUA: z ∈ ⋃ FamA.

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

An exact proof term for the current goal is HzU.

We prove the intermediate claim HzVB: z ∈ ⋃ FamB.

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

An exact proof term for the current goal is HzV.

Apply (UnionE_impred FamA z HzUA False) to the current goal.

Let I be given.

Assume HzI: z ∈ I.

Assume HIin: I ∈ FamA.

Apply (UnionE_impred FamB z HzVB False) to the current goal.

Let J be given.

Assume HzJ: z ∈ J.

Assume HJin: J ∈ FamB.

We prove the intermediate claim HIopen: I ∈ order_topology X.

An exact proof term for the current goal is (SepE1 (order_topology X) (λI0 : set ⇒ ∃a0 ∈ A, ∃x0 ∈ X, order_rel X x0 a0 ∧ I0 = order_interval_right_closed X x0 a0 ∧ order_interval_right_closed X x0 a0 ⊆ UB) I HIin).

We prove the intermediate claim HIprop: ∃a0 ∈ A, ∃x0 ∈ X, order_rel X x0 a0 ∧ I = order_interval_right_closed X x0 a0 ∧ order_interval_right_closed X x0 a0 ⊆ UB.

An exact proof term for the current goal is (SepE2 (order_topology X) (λI0 : set ⇒ ∃a0 ∈ A, ∃x0 ∈ X, order_rel X x0 a0 ∧ I0 = order_interval_right_closed X x0 a0 ∧ order_interval_right_closed X x0 a0 ⊆ UB) I HIin).

We prove the intermediate claim HJopen: J ∈ order_topology X.

An exact proof term for the current goal is (SepE1 (order_topology X) (λJ0 : set ⇒ ∃b0 ∈ B, ∃y0 ∈ X, order_rel X y0 b0 ∧ J0 = order_interval_right_closed X y0 b0 ∧ order_interval_right_closed X y0 b0 ⊆ VA) J HJin).

We prove the intermediate claim HJprop: ∃b0 ∈ B, ∃y0 ∈ X, order_rel X y0 b0 ∧ J = order_interval_right_closed X y0 b0 ∧ order_interval_right_closed X y0 b0 ⊆ VA.

An exact proof term for the current goal is (SepE2 (order_topology X) (λJ0 : set ⇒ ∃b0 ∈ B, ∃y0 ∈ X, order_rel X y0 b0 ∧ J0 = order_interval_right_closed X y0 b0 ∧ order_interval_right_closed X y0 b0 ⊆ VA) J HJin).

Apply HIprop to the current goal.

Let a0 be given.

Assume Ha0Core.

Apply Ha0Core to the current goal.

Assume Ha0A Hx0Ex.

Apply Hx0Ex to the current goal.

Let x0 be given.

Assume Hx0Core.

Apply Hx0Core to the current goal.

Assume Hx0X HIAux.

We prove the intermediate claim Ha0X: a0 ∈ X.

An exact proof term for the current goal is (HAsubX a0 Ha0A).

We prove the intermediate claim HIAux12: order_rel X x0 a0 ∧ I = order_interval_right_closed X x0 a0.

An exact proof term for the current goal is (andEL (order_rel X x0 a0 ∧ I = order_interval_right_closed X x0 a0) (order_interval_right_closed X x0 a0 ⊆ UB) HIAux).

We prove the intermediate claim HIsubUB: order_interval_right_closed X x0 a0 ⊆ UB.

An exact proof term for the current goal is (andER (order_rel X x0 a0 ∧ I = order_interval_right_closed X x0 a0) (order_interval_right_closed X x0 a0 ⊆ UB) HIAux).

We prove the intermediate claim Hx0a0: order_rel X x0 a0.

An exact proof term for the current goal is (andEL (order_rel X x0 a0) (I = order_interval_right_closed X x0 a0) HIAux12).

We prove the intermediate claim HIeq: I = order_interval_right_closed X x0 a0.

An exact proof term for the current goal is (andER (order_rel X x0 a0) (I = order_interval_right_closed X x0 a0) HIAux12).

Apply HJprop to the current goal.

Let b0 be given.

Assume Hb0Core.

Apply Hb0Core to the current goal.

Assume Hb0B Hy0Ex.

Apply Hy0Ex to the current goal.

Let y0 be given.

Assume Hy0Core.

Apply Hy0Core to the current goal.

Assume Hy0X HJAux.

We prove the intermediate claim Hb0X: b0 ∈ X.

An exact proof term for the current goal is (HBsubX b0 Hb0B).

We prove the intermediate claim HJAux12: order_rel X y0 b0 ∧ J = order_interval_right_closed X y0 b0.

An exact proof term for the current goal is (andEL (order_rel X y0 b0 ∧ J = order_interval_right_closed X y0 b0) (order_interval_right_closed X y0 b0 ⊆ VA) HJAux).

We prove the intermediate claim HJsubVA: order_interval_right_closed X y0 b0 ⊆ VA.

An exact proof term for the current goal is (andER (order_rel X y0 b0 ∧ J = order_interval_right_closed X y0 b0) (order_interval_right_closed X y0 b0 ⊆ VA) HJAux).

We prove the intermediate claim Hy0b0: order_rel X y0 b0.

An exact proof term for the current goal is (andEL (order_rel X y0 b0) (J = order_interval_right_closed X y0 b0) HJAux12).

We prove the intermediate claim HJeq: J = order_interval_right_closed X y0 b0.

An exact proof term for the current goal is (andER (order_rel X y0 b0) (J = order_interval_right_closed X y0 b0) HJAux12).

We prove the intermediate claim HzI': z ∈ order_interval_right_closed X x0 a0.

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

An exact proof term for the current goal is HzI.

We prove the intermediate claim HzJ': z ∈ order_interval_right_closed X y0 b0.

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

An exact proof term for the current goal is HzJ.

We prove the intermediate claim HzX: z ∈ X.

An exact proof term for the current goal is (SepE1 X (λz0 : set ⇒ order_rel X x0 z0 ∧ (z0 = a0 ∨ order_rel X z0 a0)) z HzI').

We prove the intermediate claim HzDataA: order_rel X x0 z ∧ (z = a0 ∨ order_rel X z a0).

An exact proof term for the current goal is (SepE2 X (λz0 : set ⇒ order_rel X x0 z0 ∧ (z0 = a0 ∨ order_rel X z0 a0)) z HzI').

We prove the intermediate claim HzleA: z = a0 ∨ order_rel X z a0.

An exact proof term for the current goal is (andER (order_rel X x0 z) (z = a0 ∨ order_rel X z a0) HzDataA).

We prove the intermediate claim HzDataB: order_rel X y0 z ∧ (z = b0 ∨ order_rel X z b0).

An exact proof term for the current goal is (SepE2 X (λz0 : set ⇒ order_rel X y0 z0 ∧ (z0 = b0 ∨ order_rel X z0 b0)) z HzJ').

We prove the intermediate claim Hy0z: order_rel X y0 z.

An exact proof term for the current goal is (andEL (order_rel X y0 z) (z = b0 ∨ order_rel X z b0) HzDataB).

We prove the intermediate claim HzleB: z = b0 ∨ order_rel X z b0.

An exact proof term for the current goal is (andER (order_rel X y0 z) (z = b0 ∨ order_rel X z b0) HzDataB).

Apply (order_rel_trichotomy_or_impred X a0 b0 Hso Ha0X Hb0X False) to the current goal.

Assume Ha0b0: order_rel X a0 b0.

Apply (order_rel_trichotomy_or_impred X a0 y0 Hso Ha0X Hy0X False) to the current goal.

Assume Ha0y0: order_rel X a0 y0.

We prove the intermediate claim Hzy0: order_rel X z y0.

Apply HzleA to the current goal.

Assume Hza0: z = a0.

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

An exact proof term for the current goal is Ha0y0.

Assume HzltA: order_rel X z a0.

An exact proof term for the current goal is (order_rel_trans X z a0 y0 Hso HzX Ha0X Hy0X HzltA Ha0y0).

We prove the intermediate claim Hy0y0: order_rel X y0 y0.

An exact proof term for the current goal is (order_rel_trans X y0 z y0 Hso Hy0X HzX Hy0X Hy0z Hzy0).

An exact proof term for the current goal is ((order_rel_irref X y0) Hy0y0).

Assume Ha0eqy0: a0 = y0.

We prove the intermediate claim Hzy0: z = y0 ∨ order_rel X z y0.

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

An exact proof term for the current goal is HzleA.

Apply Hzy0 to the current goal.

Assume Hzy0eq: z = y0.

We prove the intermediate claim Hy0y0: order_rel X y0 y0.

An exact proof term for the current goal is (Hzy0eq (λu v : set ⇒ order_rel X y0 u) Hy0z).

An exact proof term for the current goal is ((order_rel_irref X y0) Hy0y0).

Assume Hzy0lt: order_rel X z y0.

We prove the intermediate claim Hy0y0: order_rel X y0 y0.

An exact proof term for the current goal is (order_rel_trans X y0 z y0 Hso Hy0X HzX Hy0X Hy0z Hzy0lt).

An exact proof term for the current goal is ((order_rel_irref X y0) Hy0y0).

Assume Hy0a0: order_rel X y0 a0.

We prove the intermediate claim Ha0J: a0 ∈ order_interval_right_closed X y0 b0.

We prove the intermediate claim HJdef': order_interval_right_closed X y0 b0 = {t ∈ X|order_rel X y0 t ∧ (t = b0 ∨ order_rel X t b0)}.

Use reflexivity.

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

Apply (SepI X (λt : set ⇒ order_rel X y0 t ∧ (t = b0 ∨ order_rel X t b0)) a0 Ha0X) to the current goal.

Apply andI to the current goal.

An exact proof term for the current goal is Hy0a0.

Apply orIR to the current goal.

An exact proof term for the current goal is Ha0b0.

We prove the intermediate claim Ha0VA: a0 ∈ VA.

An exact proof term for the current goal is (HJsubVA a0 Ha0J).

We prove the intermediate claim Ha0NotVA: a0 ∉ VA.

We prove the intermediate claim Ha0XVA: a0 ∈ X ∖ VA.

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

An exact proof term for the current goal is Ha0A.

An exact proof term for the current goal is (setminusE2 X VA a0 Ha0XVA).

An exact proof term for the current goal is (Ha0NotVA Ha0VA).

Assume Ha0eqb0: a0 = b0.

We prove the intermediate claim Ha0AB: a0 ∈ A ∩ B.

Apply (binintersectI A B a0 Ha0A) to the current goal.

We prove the intermediate claim Hb0eqa0: b0 = a0.

Use symmetry.

An exact proof term for the current goal is Ha0eqb0.

An exact proof term for the current goal is (Hb0eqa0 (λu v : set ⇒ u ∈ B) Hb0B).

We prove the intermediate claim Ha0E: a0 ∈ Empty.

An exact proof term for the current goal is (HABdisj (λU0 V0 : set ⇒ a0 ∈ U0) Ha0AB).

An exact proof term for the current goal is (EmptyE a0 Ha0E False).

Assume Hb0a0: order_rel X b0 a0.

Apply (order_rel_trichotomy_or_impred X b0 x0 Hso Hb0X Hx0X False) to the current goal.

Assume Hb0x0: order_rel X b0 x0.

We prove the intermediate claim Hzx0: order_rel X z x0.

Apply HzleB to the current goal.

Assume Hzb0: z = b0.

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

An exact proof term for the current goal is Hb0x0.

Assume HzltB: order_rel X z b0.

An exact proof term for the current goal is (order_rel_trans X z b0 x0 Hso HzX Hb0X Hx0X HzltB Hb0x0).

We prove the intermediate claim Hx0x0: order_rel X x0 x0.

An exact proof term for the current goal is (order_rel_trans X x0 z x0 Hso Hx0X HzX Hx0X (andEL (order_rel X x0 z) (z = a0 ∨ order_rel X z a0) HzDataA) Hzx0).

An exact proof term for the current goal is ((order_rel_irref X x0) Hx0x0).

Assume Hb0eqx0: b0 = x0.

We prove the intermediate claim Hzx0: z = x0 ∨ order_rel X z x0.

An exact proof term for the current goal is (Hb0eqx0 (λu v : set ⇒ z = u ∨ order_rel X z u) HzleB).

Apply Hzx0 to the current goal.

Assume Hzx0eq: z = x0.

We prove the intermediate claim Hx0z: order_rel X x0 z.

An exact proof term for the current goal is (andEL (order_rel X x0 z) (z = a0 ∨ order_rel X z a0) HzDataA).

We prove the intermediate claim Hx0x0: order_rel X x0 x0.

An exact proof term for the current goal is (Hzx0eq (λu v : set ⇒ order_rel X x0 u) Hx0z).

An exact proof term for the current goal is ((order_rel_irref X x0) Hx0x0).

Assume Hzx0lt: order_rel X z x0.

We prove the intermediate claim Hx0x0: order_rel X x0 x0.

An exact proof term for the current goal is (order_rel_trans X x0 z x0 Hso Hx0X HzX Hx0X (andEL (order_rel X x0 z) (z = a0 ∨ order_rel X z a0) HzDataA) Hzx0lt).

An exact proof term for the current goal is ((order_rel_irref X x0) Hx0x0).

Assume Hx0b0: order_rel X x0 b0.

We prove the intermediate claim Hb0I: b0 ∈ order_interval_right_closed X x0 a0.

We prove the intermediate claim HIdef': order_interval_right_closed X x0 a0 = {t ∈ X|order_rel X x0 t ∧ (t = a0 ∨ order_rel X t a0)}.

Use reflexivity.

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

Apply (SepI X (λt : set ⇒ order_rel X x0 t ∧ (t = a0 ∨ order_rel X t a0)) b0 Hb0X) to the current goal.

Apply andI to the current goal.

An exact proof term for the current goal is Hx0b0.

Apply orIR to the current goal.

An exact proof term for the current goal is Hb0a0.

We prove the intermediate claim Hb0UB: b0 ∈ UB.

An exact proof term for the current goal is (HIsubUB b0 Hb0I).

We prove the intermediate claim Hb0NotUB: b0 ∉ UB.

We prove the intermediate claim Hb0XUB: b0 ∈ X ∖ UB.

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

An exact proof term for the current goal is Hb0B.

An exact proof term for the current goal is (setminusE2 X UB b0 Hb0XUB).

An exact proof term for the current goal is (Hb0NotUB Hb0UB).