Let X, a, b, x and b0 be given.
Assume Hso: simply_ordered_set X.
Assume Ha: a ∈ X.
Assume Hb: b ∈ X.
Assume Hab: order_rel X a b.
Assume Hsucc: no_immediate_successor X a.
Assume Hpred: no_immediate_predecessor X b.
Assume Hx: x ∈ closed_interval_in X a b.
Assume Hb0B: b0 ∈ order_topology_basis X.
Assume Hxb0: x ∈ b0.
We will prove ∃y : set, y ∈ b0 ∧ y ∈ order_interval X a b.
Set FamInt to be the term {I ∈ 𝒫 X|∃a0 ∈ X, ∃b0x ∈ X, I = {x0 ∈ X|order_rel X a0 x0 ∧ order_rel X x0 b0x}}.
Set FamLow to be the term {I ∈ 𝒫 X|∃b0x ∈ X, I = {x0 ∈ X|order_rel X x0 b0x}}.
Set FamUp to be the term {I ∈ 𝒫 X|∃a0 ∈ X, I = {x0 ∈ X|order_rel X a0 x0}}.
Set Bold to be the term (FamInt ∪ FamLow) ∪ FamUp.
We prove the intermediate claim Hb0BX: b0 ∈ Bold ∪ {X}.
An exact proof term for the current goal is Hb0B.
Apply (binunionE Bold {X} b0 Hb0BX) to the current goal.
Assume Hb0Bold: b0 ∈ Bold.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ (x0 = a ∨ order_rel X a x0) ∧ (x0 = b ∨ order_rel X x0 b)) x Hx).
We prove the intermediate claim Hcond: (x = a ∨ order_rel X a x) ∧ (x = b ∨ order_rel X x b).
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ (x0 = a ∨ order_rel X a x0) ∧ (x0 = b ∨ order_rel X x0 b)) x Hx).
We prove the intermediate claim Hleft: x = a ∨ order_rel X a x.
An exact proof term for the current goal is (andEL (x = a ∨ order_rel X a x) (x = b ∨ order_rel X x b) Hcond).
We prove the intermediate claim Hright: x = b ∨ order_rel X x b.
An exact proof term for the current goal is (andER (x = a ∨ order_rel X a x) (x = b ∨ order_rel X x b) Hcond).
Apply (binunionE (FamInt ∪ FamLow) FamUp b0 Hb0Bold) to the current goal.
Assume Hb0IntLow: b0 ∈ FamInt ∪ FamLow.
Apply (binunionE FamInt FamLow b0 Hb0IntLow) to the current goal.
Assume Hb0Int: b0 ∈ FamInt.
We prove the intermediate claim Hex: ∃a0 ∈ X, ∃b1 ∈ X, b0 = {x0 ∈ X|order_rel X a0 x0 ∧ order_rel X x0 b1}.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λI : set ⇒ ∃a0 ∈ X, ∃b1 ∈ X, I = {x0 ∈ X|order_rel X a0 x0 ∧ order_rel X x0 b1}) b0 Hb0Int).
Apply Hex to the current goal.
Let a0 be given.
Assume Ha0core.
Apply Ha0core to the current goal.
Assume Ha0X Ha0rest.
Apply Ha0rest to the current goal.
Let b1 be given.
Assume Hb1core.
Apply Hb1core to the current goal.
Assume Hb1X Hb0def.
We prove the intermediate claim HxIn: x ∈ {x0 ∈ X|order_rel X a0 x0 ∧ order_rel X x0 b1}.
rewrite the current goal using Hb0def (from right to left).
An exact proof term for the current goal is Hxb0.
We prove the intermediate claim HxProp: order_rel X a0 x ∧ order_rel X x b1.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X a0 x0 ∧ order_rel X x0 b1) x HxIn).
We prove the intermediate claim Ha0x: order_rel X a0 x.
An exact proof term for the current goal is (andEL (order_rel X a0 x) (order_rel X x b1) HxProp).
We prove the intermediate claim Hxb1: order_rel X x b1.
An exact proof term for the current goal is (andER (order_rel X a0 x) (order_rel X x b1) HxProp).
Apply Hleft to the current goal.
Assume Hxa: x = a.
We prove the intermediate claim Ha0a: order_rel X a0 a.
rewrite the current goal using Hxa (from right to left).
An exact proof term for the current goal is Ha0x.
We prove the intermediate claim Hab1: order_rel X a b1.
rewrite the current goal using Hxa (from right to left).
An exact proof term for the current goal is Hxb1.
Apply (order_rel_trichotomy_or_impred X b1 b Hso Hb1X Hb (∃y : set, y ∈ b0 ∧ y ∈ order_interval X a b)) to the current goal.
Assume Hb1ltb: order_rel X b1 b.
We prove the intermediate claim Hexy0: ∃y : set, y ∈ X ∧ order_rel X a y ∧ order_rel X y b1.
An exact proof term for the current goal is (Hsucc b1 Hb1X Hab1).
Apply Hexy0 to the current goal.
Let y be given.
Assume Hycore.
Apply Hycore to the current goal.
Assume HyXpair Hyb1.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (andEL (y ∈ X) (order_rel X a y) HyXpair).
We prove the intermediate claim Hay: order_rel X a y.
An exact proof term for the current goal is (andER (y ∈ X) (order_rel X a y) HyXpair).
We prove the intermediate claim Ha0y: order_rel X a0 y.
An exact proof term for the current goal is (order_rel_trans X a0 a y Hso Ha0X Ha HyX Ha0a Hay).
We prove the intermediate claim Hyb: order_rel X y b.
An exact proof term for the current goal is (order_rel_trans X y b1 b Hso HyX Hb1X Hb Hyb1 Hb1ltb).
We use y to witness the existential quantifier.
Apply andI to the current goal.
We will prove y ∈ b0.
rewrite the current goal using Hb0def (from left to right).
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ order_rel X a0 x0 ∧ order_rel X x0 b1) y HyX (andI (order_rel X a0 y) (order_rel X y b1) Ha0y Hyb1)).
We will prove y ∈ order_interval X a b.
An exact proof term for the current goal is (order_intervalI X a b y HyX Hay Hyb).
Assume Hb1eq: b1 = b.
We prove the intermediate claim Hexy0: ∃y : set, y ∈ X ∧ order_rel X a y ∧ order_rel X y b.
An exact proof term for the current goal is (Hsucc b Hb Hab).
Apply Hexy0 to the current goal.
Let y be given.
Assume Hycore.
Apply Hycore to the current goal.
Assume HyXpair Hyb.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (andEL (y ∈ X) (order_rel X a y) HyXpair).
We prove the intermediate claim Hay: order_rel X a y.
An exact proof term for the current goal is (andER (y ∈ X) (order_rel X a y) HyXpair).
We prove the intermediate claim Ha0y: order_rel X a0 y.
An exact proof term for the current goal is (order_rel_trans X a0 a y Hso Ha0X Ha HyX Ha0a Hay).
We prove the intermediate claim Hyb1: order_rel X y b1.
rewrite the current goal using Hb1eq (from left to right).
An exact proof term for the current goal is Hyb.
We use y to witness the existential quantifier.
Apply andI to the current goal.
We will prove y ∈ b0.
rewrite the current goal using Hb0def (from left to right).
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ order_rel X a0 x0 ∧ order_rel X x0 b1) y HyX (andI (order_rel X a0 y) (order_rel X y b1) Ha0y Hyb1)).
We will prove y ∈ order_interval X a b.
An exact proof term for the current goal is (order_intervalI X a b y HyX Hay Hyb).
Assume Hbltb1: order_rel X b b1.
We prove the intermediate claim Hexy0: ∃y : set, y ∈ X ∧ order_rel X a y ∧ order_rel X y b.
An exact proof term for the current goal is (Hsucc b Hb Hab).
Apply Hexy0 to the current goal.
Let y be given.
Assume Hycore.
Apply Hycore to the current goal.
Assume HyXpair Hyb.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (andEL (y ∈ X) (order_rel X a y) HyXpair).
We prove the intermediate claim Hay: order_rel X a y.
An exact proof term for the current goal is (andER (y ∈ X) (order_rel X a y) HyXpair).
We prove the intermediate claim Ha0y: order_rel X a0 y.
An exact proof term for the current goal is (order_rel_trans X a0 a y Hso Ha0X Ha HyX Ha0a Hay).
We prove the intermediate claim Hyb1: order_rel X y b1.
An exact proof term for the current goal is (order_rel_trans X y b b1 Hso HyX Hb Hb1X Hyb Hbltb1).
We use y to witness the existential quantifier.
Apply andI to the current goal.
We will prove y ∈ b0.
rewrite the current goal using Hb0def (from left to right).
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ order_rel X a0 x0 ∧ order_rel X x0 b1) y HyX (andI (order_rel X a0 y) (order_rel X y b1) Ha0y Hyb1)).
We will prove y ∈ order_interval X a b.
An exact proof term for the current goal is (order_intervalI X a b y HyX Hay Hyb).
Assume Hax: order_rel X a x.
Apply Hright to the current goal.
Assume Hxb: x = b.
We prove the intermediate claim Hb1gtb: order_rel X b b1.
rewrite the current goal using Hxb (from right to left).
An exact proof term for the current goal is Hxb1.
Apply (order_rel_trichotomy_or_impred X a0 a Hso Ha0X Ha (∃y : set, y ∈ b0 ∧ y ∈ order_interval X a b)) to the current goal.
Assume Ha0lta: order_rel X a0 a.
We prove the intermediate claim Hexy0: ∃y : set, y ∈ X ∧ order_rel X a y ∧ order_rel X y b.
An exact proof term for the current goal is (Hpred a Ha Hab).
Apply Hexy0 to the current goal.
Let y be given.
Assume Hycore.
Apply Hycore to the current goal.
Assume HyXpair Hyb.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (andEL (y ∈ X) (order_rel X a y) HyXpair).
We prove the intermediate claim Hay: order_rel X a y.
An exact proof term for the current goal is (andER (y ∈ X) (order_rel X a y) HyXpair).
We prove the intermediate claim Ha0y: order_rel X a0 y.
An exact proof term for the current goal is (order_rel_trans X a0 a y Hso Ha0X Ha HyX Ha0lta Hay).
We prove the intermediate claim Hyb1: order_rel X y b1.
An exact proof term for the current goal is (order_rel_trans X y b b1 Hso HyX Hb Hb1X Hyb Hb1gtb).
We use y to witness the existential quantifier.
Apply andI to the current goal.
We will prove y ∈ b0.
rewrite the current goal using Hb0def (from left to right).
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ order_rel X a0 x0 ∧ order_rel X x0 b1) y HyX (andI (order_rel X a0 y) (order_rel X y b1) Ha0y Hyb1)).
We will prove y ∈ order_interval X a b.
An exact proof term for the current goal is (order_intervalI X a b y HyX Hay Hyb).
Assume Ha0eq: a0 = a.
We prove the intermediate claim Hexy0: ∃y : set, y ∈ X ∧ order_rel X a y ∧ order_rel X y b.
An exact proof term for the current goal is (Hpred a Ha Hab).
Apply Hexy0 to the current goal.
Let y be given.
Assume Hycore.
Apply Hycore to the current goal.
Assume HyXpair Hyb.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (andEL (y ∈ X) (order_rel X a y) HyXpair).
We prove the intermediate claim Hay: order_rel X a y.
An exact proof term for the current goal is (andER (y ∈ X) (order_rel X a y) HyXpair).
We prove the intermediate claim Ha0y: order_rel X a0 y.
rewrite the current goal using Ha0eq (from left to right).
An exact proof term for the current goal is Hay.
We prove the intermediate claim Hyb1: order_rel X y b1.
An exact proof term for the current goal is (order_rel_trans X y b b1 Hso HyX Hb Hb1X Hyb Hb1gtb).
We use y to witness the existential quantifier.
Apply andI to the current goal.
We will prove y ∈ b0.
rewrite the current goal using Hb0def (from left to right).
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ order_rel X a0 x0 ∧ order_rel X x0 b1) y HyX (andI (order_rel X a0 y) (order_rel X y b1) Ha0y Hyb1)).
We will prove y ∈ order_interval X a b.
An exact proof term for the current goal is (order_intervalI X a b y HyX Hay Hyb).
Assume Halta0: order_rel X a a0.
We prove the intermediate claim Hlt: order_rel X a0 b.
rewrite the current goal using Hxb (from right to left).
An exact proof term for the current goal is Ha0x.
We prove the intermediate claim Hexy0: ∃y : set, y ∈ X ∧ order_rel X a0 y ∧ order_rel X y b.
An exact proof term for the current goal is (Hpred a0 Ha0X Hlt).
Apply Hexy0 to the current goal.
Let y be given.
Assume Hycore.
Apply Hycore to the current goal.
Assume HyXpair Hyb.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (andEL (y ∈ X) (order_rel X a0 y) HyXpair).
We prove the intermediate claim Ha0y: order_rel X a0 y.
An exact proof term for the current goal is (andER (y ∈ X) (order_rel X a0 y) HyXpair).
We prove the intermediate claim Hay: order_rel X a y.
An exact proof term for the current goal is (order_rel_trans X a a0 y Hso Ha Ha0X HyX Halta0 Ha0y).
We prove the intermediate claim Hyb1: order_rel X y b1.
An exact proof term for the current goal is (order_rel_trans X y b b1 Hso HyX Hb Hb1X Hyb Hb1gtb).
We use y to witness the existential quantifier.
Apply andI to the current goal.
We will prove y ∈ b0.
rewrite the current goal using Hb0def (from left to right).
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ order_rel X a0 x0 ∧ order_rel X x0 b1) y HyX (andI (order_rel X a0 y) (order_rel X y b1) Ha0y Hyb1)).
We will prove y ∈ order_interval X a b.
An exact proof term for the current goal is (order_intervalI X a b y HyX Hay Hyb).
Assume Hxb: order_rel X x b.
We use x to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hxb0.
An exact proof term for the current goal is (order_intervalI X a b x HxX Hax Hxb).
Assume Hb0Low: b0 ∈ FamLow.
We prove the intermediate claim Hex: ∃b1 ∈ X, b0 = {x0 ∈ X|order_rel X x0 b1}.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λI : set ⇒ ∃b1 ∈ X, I = {x0 ∈ X|order_rel X x0 b1}) b0 Hb0Low).
Apply Hex to the current goal.
Let b1 be given.
Assume Hb1core.
Apply Hb1core to the current goal.
Assume Hb1X Hb0def.
We prove the intermediate claim HxIn: x ∈ {x0 ∈ X|order_rel X x0 b1}.
rewrite the current goal using Hb0def (from right to left).
An exact proof term for the current goal is Hxb0.
We prove the intermediate claim Hxb1: order_rel X x b1.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X x0 b1) x HxIn).
Apply Hleft to the current goal.
Assume Hxa: x = a.
We prove the intermediate claim Hab1: order_rel X a b1.
rewrite the current goal using Hxa (from right to left).
An exact proof term for the current goal is Hxb1.
Apply (order_rel_trichotomy_or_impred X b1 b Hso Hb1X Hb (∃y : set, y ∈ b0 ∧ y ∈ order_interval X a b)) to the current goal.
Assume Hb1ltb: order_rel X b1 b.
We prove the intermediate claim Hexy0: ∃y : set, y ∈ X ∧ order_rel X a y ∧ order_rel X y b1.
An exact proof term for the current goal is (Hsucc b1 Hb1X Hab1).
Apply Hexy0 to the current goal.
Let y be given.
Assume Hycore.
Apply Hycore to the current goal.
Assume HyXpair Hyb1.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (andEL (y ∈ X) (order_rel X a y) HyXpair).
We prove the intermediate claim Hay: order_rel X a y.
An exact proof term for the current goal is (andER (y ∈ X) (order_rel X a y) HyXpair).
We prove the intermediate claim Hyb: order_rel X y b.
An exact proof term for the current goal is (order_rel_trans X y b1 b Hso HyX Hb1X Hb Hyb1 Hb1ltb).
We use y to witness the existential quantifier.
Apply andI to the current goal.
We will prove y ∈ b0.
rewrite the current goal using Hb0def (from left to right).
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ order_rel X x0 b1) y HyX Hyb1).
We will prove y ∈ order_interval X a b.
An exact proof term for the current goal is (order_intervalI X a b y HyX Hay Hyb).
Assume Hb1eq: b1 = b.
We prove the intermediate claim Hexy0: ∃y : set, y ∈ X ∧ order_rel X a y ∧ order_rel X y b.
An exact proof term for the current goal is (Hsucc b Hb Hab).
Apply Hexy0 to the current goal.
Let y be given.
Assume Hycore.
Apply Hycore to the current goal.
Assume HyXpair Hyb.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (andEL (y ∈ X) (order_rel X a y) HyXpair).
We prove the intermediate claim Hay: order_rel X a y.
An exact proof term for the current goal is (andER (y ∈ X) (order_rel X a y) HyXpair).
We prove the intermediate claim Hyb1: order_rel X y b1.
rewrite the current goal using Hb1eq (from left to right).
An exact proof term for the current goal is Hyb.
We use y to witness the existential quantifier.
Apply andI to the current goal.
We will prove y ∈ b0.
rewrite the current goal using Hb0def (from left to right).
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ order_rel X x0 b1) y HyX Hyb1).
We will prove y ∈ order_interval X a b.
An exact proof term for the current goal is (order_intervalI X a b y HyX Hay Hyb).
Assume Hbltb1: order_rel X b b1.
We prove the intermediate claim Hexy0: ∃y : set, y ∈ X ∧ order_rel X a y ∧ order_rel X y b.
An exact proof term for the current goal is (Hsucc b Hb Hab).
Apply Hexy0 to the current goal.
Let y be given.
Assume Hycore.
Apply Hycore to the current goal.
Assume HyXpair Hyb.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (andEL (y ∈ X) (order_rel X a y) HyXpair).
We prove the intermediate claim Hay: order_rel X a y.
An exact proof term for the current goal is (andER (y ∈ X) (order_rel X a y) HyXpair).
We prove the intermediate claim Hyb1: order_rel X y b1.
An exact proof term for the current goal is (order_rel_trans X y b b1 Hso HyX Hb Hb1X Hyb Hbltb1).
We use y to witness the existential quantifier.
Apply andI to the current goal.
We will prove y ∈ b0.
rewrite the current goal using Hb0def (from left to right).
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ order_rel X x0 b1) y HyX Hyb1).
We will prove y ∈ order_interval X a b.
An exact proof term for the current goal is (order_intervalI X a b y HyX Hay Hyb).
Assume Hax: order_rel X a x.
Apply Hright to the current goal.
Assume Hxb: x = b.
We prove the intermediate claim Hb1gtb: order_rel X b b1.
rewrite the current goal using Hxb (from right to left).
An exact proof term for the current goal is Hxb1.
We prove the intermediate claim Hexy0: ∃y : set, y ∈ X ∧ order_rel X a y ∧ order_rel X y b.
An exact proof term for the current goal is (Hpred a Ha Hab).
Apply Hexy0 to the current goal.
Let y be given.
Assume Hycore.
Apply Hycore to the current goal.
Assume HyXpair Hyb.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (andEL (y ∈ X) (order_rel X a y) HyXpair).
We prove the intermediate claim Hay: order_rel X a y.
An exact proof term for the current goal is (andER (y ∈ X) (order_rel X a y) HyXpair).
We prove the intermediate claim Hyb1: order_rel X y b1.
An exact proof term for the current goal is (order_rel_trans X y b b1 Hso HyX Hb Hb1X Hyb Hb1gtb).
We use y to witness the existential quantifier.
Apply andI to the current goal.
We will prove y ∈ b0.
rewrite the current goal using Hb0def (from left to right).
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ order_rel X x0 b1) y HyX Hyb1).
We will prove y ∈ order_interval X a b.
An exact proof term for the current goal is (order_intervalI X a b y HyX Hay Hyb).
Assume Hxb: order_rel X x b.
We use x to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hxb0.
An exact proof term for the current goal is (order_intervalI X a b x HxX Hax Hxb).
Assume Hb0Up: b0 ∈ FamUp.
We prove the intermediate claim Hex: ∃a0 ∈ X, b0 = {x0 ∈ X|order_rel X a0 x0}.
An exact proof term for the current goal is (SepE2 (𝒫 X) (λI : set ⇒ ∃a0 ∈ X, I = {x0 ∈ X|order_rel X a0 x0}) b0 Hb0Up).
Apply Hex to the current goal.
Let a0 be given.
Assume Ha0core.
Apply Ha0core to the current goal.
Assume Ha0X Hb0def.
We prove the intermediate claim HxIn: x ∈ {x0 ∈ X|order_rel X a0 x0}.
rewrite the current goal using Hb0def (from right to left).
An exact proof term for the current goal is Hxb0.
We prove the intermediate claim Ha0x: order_rel X a0 x.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X a0 x0) x HxIn).
Apply Hleft to the current goal.
Assume Hxa: x = a.
We prove the intermediate claim Ha0a: order_rel X a0 a.
rewrite the current goal using Hxa (from right to left).
An exact proof term for the current goal is Ha0x.
We prove the intermediate claim Hexy0: ∃y : set, y ∈ X ∧ order_rel X a y ∧ order_rel X y b.
An exact proof term for the current goal is (Hsucc b Hb Hab).
Apply Hexy0 to the current goal.
Let y be given.
Assume Hycore.
Apply Hycore to the current goal.
Assume HyXpair Hyb.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (andEL (y ∈ X) (order_rel X a y) HyXpair).
We prove the intermediate claim Hay: order_rel X a y.
An exact proof term for the current goal is (andER (y ∈ X) (order_rel X a y) HyXpair).
We prove the intermediate claim Ha0y: order_rel X a0 y.
An exact proof term for the current goal is (order_rel_trans X a0 a y Hso Ha0X Ha HyX Ha0a Hay).
We use y to witness the existential quantifier.
Apply andI to the current goal.
We will prove y ∈ b0.
rewrite the current goal using Hb0def (from left to right).
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ order_rel X a0 x0) y HyX Ha0y).
We will prove y ∈ order_interval X a b.
An exact proof term for the current goal is (order_intervalI X a b y HyX Hay Hyb).
Assume Hax: order_rel X a x.
Apply Hright to the current goal.
Assume Hxb: x = b.
We prove the intermediate claim Ha0b: order_rel X a0 b.
rewrite the current goal using Hxb (from right to left).
An exact proof term for the current goal is Ha0x.
Apply (order_rel_trichotomy_or_impred X a0 a Hso Ha0X Ha (∃y : set, y ∈ b0 ∧ y ∈ order_interval X a b)) to the current goal.
Assume Ha0lta: order_rel X a0 a.
We prove the intermediate claim Hexy0: ∃y : set, y ∈ X ∧ order_rel X a y ∧ order_rel X y b.
An exact proof term for the current goal is (Hpred a Ha Hab).
Apply Hexy0 to the current goal.
Let y be given.
Assume Hycore.
Apply Hycore to the current goal.
Assume HyXpair Hyb.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (andEL (y ∈ X) (order_rel X a y) HyXpair).
We prove the intermediate claim Hay: order_rel X a y.
An exact proof term for the current goal is (andER (y ∈ X) (order_rel X a y) HyXpair).
We prove the intermediate claim Ha0y: order_rel X a0 y.
An exact proof term for the current goal is (order_rel_trans X a0 a y Hso Ha0X Ha HyX Ha0lta Hay).
We use y to witness the existential quantifier.
Apply andI to the current goal.
We will prove y ∈ b0.
rewrite the current goal using Hb0def (from left to right).
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ order_rel X a0 x0) y HyX Ha0y).
We will prove y ∈ order_interval X a b.
An exact proof term for the current goal is (order_intervalI X a b y HyX Hay Hyb).
Assume Ha0eq: a0 = a.
We prove the intermediate claim Hexy0: ∃y : set, y ∈ X ∧ order_rel X a y ∧ order_rel X y b.
An exact proof term for the current goal is (Hpred a Ha Hab).
Apply Hexy0 to the current goal.
Let y be given.
Assume Hycore.
Apply Hycore to the current goal.
Assume HyXpair Hyb.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (andEL (y ∈ X) (order_rel X a y) HyXpair).
We prove the intermediate claim Hay: order_rel X a y.
An exact proof term for the current goal is (andER (y ∈ X) (order_rel X a y) HyXpair).
We prove the intermediate claim Ha0y: order_rel X a0 y.
rewrite the current goal using Ha0eq (from left to right).
An exact proof term for the current goal is Hay.
We use y to witness the existential quantifier.
Apply andI to the current goal.
We will prove y ∈ b0.
rewrite the current goal using Hb0def (from left to right).
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ order_rel X a0 x0) y HyX Ha0y).
We will prove y ∈ order_interval X a b.
An exact proof term for the current goal is (order_intervalI X a b y HyX Hay Hyb).
Assume Halta0: order_rel X a a0.
We prove the intermediate claim Hexy0: ∃y : set, y ∈ X ∧ order_rel X a0 y ∧ order_rel X y b.
An exact proof term for the current goal is (Hpred a0 Ha0X Ha0b).
Apply Hexy0 to the current goal.
Let y be given.
Assume Hycore.
Apply Hycore to the current goal.
Assume HyXpair Hyb.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (andEL (y ∈ X) (order_rel X a0 y) HyXpair).
We prove the intermediate claim Ha0y: order_rel X a0 y.
An exact proof term for the current goal is (andER (y ∈ X) (order_rel X a0 y) HyXpair).
We prove the intermediate claim Hay: order_rel X a y.
An exact proof term for the current goal is (order_rel_trans X a a0 y Hso Ha Ha0X HyX Halta0 Ha0y).
We use y to witness the existential quantifier.
Apply andI to the current goal.
We will prove y ∈ b0.
rewrite the current goal using Hb0def (from left to right).
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ order_rel X a0 x0) y HyX Ha0y).
We will prove y ∈ order_interval X a b.
An exact proof term for the current goal is (order_intervalI X a b y HyX Hay Hyb).
Assume Hxb: order_rel X x b.
We use x to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hxb0.
An exact proof term for the current goal is (order_intervalI X a b x HxX Hax Hxb).
Assume Hb0X: b0 ∈ {X}.
We prove the intermediate claim Hb0eq: b0 = X.
An exact proof term for the current goal is (SingE X b0 Hb0X).
We prove the intermediate claim Hexy0: ∃y : set, y ∈ X ∧ order_rel X a y ∧ order_rel X y b.
An exact proof term for the current goal is (Hsucc b Hb Hab).
Apply Hexy0 to the current goal.
Let y be given.
Assume Hycore.
Apply Hycore to the current goal.
Assume HyXpair Hyb.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (andEL (y ∈ X) (order_rel X a y) HyXpair).
We prove the intermediate claim Hay: order_rel X a y.
An exact proof term for the current goal is (andER (y ∈ X) (order_rel X a y) HyXpair).
We use y to witness the existential quantifier.
Apply andI to the current goal.
We will prove y ∈ b0.
rewrite the current goal using Hb0eq (from left to right).
An exact proof term for the current goal is HyX.
We will prove y ∈ order_interval X a b.
An exact proof term for the current goal is (order_intervalI X a b y HyX Hay Hyb).
∎