Let X, Tx, a and b be given.
Assume Hlin: linear_continuum X Tx.
Assume HaX: a ∈ X.
Assume HbX: b ∈ X.
Assume Hab: order_rel X a b.
We will prove connected_space (order_interval X a b) (subspace_topology X Tx (order_interval X a b)).
Set T0 to be the term (simply_ordered_set X ∧ Tx = order_topology X) ∧ (∃x y : set, x ∈ X ∧ y ∈ X ∧ x ≠ y).
Set T1 to be the term T0 ∧ (∀x y : set, x ∈ X → y ∈ X → order_rel X x y → ∃z : set, z ∈ X ∧ order_rel X x z ∧ order_rel X z y).
Set T2 to be the term T1 ∧ (∀A : set, A ⊆ X → A ≠ Empty → (∃upper : set, upper ∈ X ∧ ∀a0 : set, a0 ∈ A → order_rel X a0 upper ∨ a0 = upper) → ∃lub : set, lub ∈ X ∧ (∀a0 : set, a0 ∈ A → order_rel X a0 lub ∨ a0 = lub) ∧ (∀bound : set, bound ∈ X → (∀a0 : set, a0 ∈ A → order_rel X a0 bound ∨ a0 = bound) → order_rel X lub bound ∨ lub = bound)).
We prove the intermediate claim HT2: T2.
An exact proof term for the current goal is Hlin.
We prove the intermediate claim Hlub: ∀A : set, A ⊆ X → A ≠ Empty → (∃upper : set, upper ∈ X ∧ ∀a0 : set, a0 ∈ A → order_rel X a0 upper ∨ a0 = upper) → ∃lub : set, lub ∈ X ∧ (∀a0 : set, a0 ∈ A → order_rel X a0 lub ∨ a0 = lub) ∧ (∀bound : set, bound ∈ X → (∀a0 : set, a0 ∈ A → order_rel X a0 bound ∨ a0 = bound) → order_rel X lub bound ∨ lub = bound).
An exact proof term for the current goal is (andER T1 (∀A : set, A ⊆ X → A ≠ Empty → (∃upper : set, upper ∈ X ∧ ∀a0 : set, a0 ∈ A → order_rel X a0 upper ∨ a0 = upper) → ∃lub : set, lub ∈ X ∧ (∀a0 : set, a0 ∈ A → order_rel X a0 lub ∨ a0 = lub) ∧ (∀bound : set, bound ∈ X → (∀a0 : set, a0 ∈ A → order_rel X a0 bound ∨ a0 = bound) → order_rel X lub bound ∨ lub = bound)) HT2).
We prove the intermediate claim HT1: T1.
An exact proof term for the current goal is (andEL T1 (∀A : set, A ⊆ X → A ≠ Empty → (∃upper : set, upper ∈ X ∧ ∀a0 : set, a0 ∈ A → order_rel X a0 upper ∨ a0 = upper) → ∃lub : set, lub ∈ X ∧ (∀a0 : set, a0 ∈ A → order_rel X a0 lub ∨ a0 = lub) ∧ (∀bound : set, bound ∈ X → (∀a0 : set, a0 ∈ A → order_rel X a0 bound ∨ a0 = bound) → order_rel X lub bound ∨ lub = bound)) HT2).
We prove the intermediate claim HT0: T0.
An exact proof term for the current goal is (andEL T0 (∀x y : set, x ∈ X → y ∈ X → order_rel X x y → ∃z : set, z ∈ X ∧ order_rel X x z ∧ order_rel X z y) HT1).
We prove the intermediate claim Hbetween: ∀x y : set, x ∈ X → y ∈ X → order_rel X x y → ∃z : set, z ∈ X ∧ order_rel X x z ∧ order_rel X z y.
An exact proof term for the current goal is (andER T0 (∀x y : set, x ∈ X → y ∈ X → order_rel X x y → ∃z : set, z ∈ X ∧ order_rel X x z ∧ order_rel X z y) HT1).
We prove the intermediate claim HsoEq: simply_ordered_set X ∧ Tx = order_topology X.
An exact proof term for the current goal is (andEL (simply_ordered_set X ∧ Tx = order_topology X) (∃x y : set, x ∈ X ∧ y ∈ X ∧ x ≠ y) HT0).
We prove the intermediate claim Hso: simply_ordered_set X.
An exact proof term for the current goal is (andEL (simply_ordered_set X) (Tx = order_topology X) HsoEq).
We prove the intermediate claim HTxeq: Tx = order_topology X.
An exact proof term for the current goal is (andER (simply_ordered_set X) (Tx = order_topology X) HsoEq).
rewrite the current goal using HTxeq (from left to right).
Set Tx0 to be the term order_topology X.
Set I to be the term order_interval X a b.
Set TI to be the term subspace_topology X Tx0 I.
We will prove topology_on I TI ∧ ¬ (∃U V : set, U ∈ TI ∧ V ∈ TI ∧ separation_of I U V).
Apply andI to the current goal.
We prove the intermediate claim HTx0: topology_on X Tx0.
An exact proof term for the current goal is (order_topology_is_topology X Hso).
We prove the intermediate claim HISub: I ⊆ X.
Let x be given.
Assume HxI: x ∈ I.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ order_rel X a x0 ∧ order_rel X x0 b) x HxI).
An exact proof term for the current goal is (subspace_topology_is_topology X Tx0 I HTx0 HISub).
Assume Hsep: ∃U V : set, U ∈ TI ∧ V ∈ TI ∧ separation_of I U V.
Apply Hsep to the current goal.
Let U be given.
Assume HexV: ∃V : set, U ∈ TI ∧ V ∈ TI ∧ separation_of I U V.
Apply HexV to the current goal.
Let V be given.
Assume HUV: U ∈ TI ∧ V ∈ TI ∧ separation_of I U V.
We prove the intermediate claim HUV0: U ∈ TI ∧ V ∈ TI.
An exact proof term for the current goal is (andEL (U ∈ TI ∧ V ∈ TI) (separation_of I U V) HUV).
We prove the intermediate claim HUinSub: U ∈ TI.
An exact proof term for the current goal is (andEL (U ∈ TI) (V ∈ TI) HUV0).
We prove the intermediate claim HVinSub: V ∈ TI.
An exact proof term for the current goal is (andER (U ∈ TI) (V ∈ TI) HUV0).
We prove the intermediate claim HsepUV: separation_of I U V.
An exact proof term for the current goal is (andER (U ∈ TI ∧ V ∈ TI) (separation_of I U V) HUV).
We prove the intermediate claim Hpart1: ((((U ∈ 𝒫 I ∧ V ∈ 𝒫 I) ∧ U ∩ V = Empty) ∧ U ≠ Empty) ∧ V ≠ Empty).
An exact proof term for the current goal is (andEL ((((U ∈ 𝒫 I ∧ V ∈ 𝒫 I) ∧ U ∩ V = Empty) ∧ U ≠ Empty) ∧ V ≠ Empty) (U ∪ V = I) HsepUV).
We prove the intermediate claim Hunion: U ∪ V = I.
An exact proof term for the current goal is (andER ((((U ∈ 𝒫 I ∧ V ∈ 𝒫 I) ∧ U ∩ V = Empty) ∧ U ≠ Empty) ∧ V ≠ Empty) (U ∪ V = I) HsepUV).
We prove the intermediate claim HAux: (((U ∈ 𝒫 I ∧ V ∈ 𝒫 I) ∧ U ∩ V = Empty) ∧ U ≠ Empty).
An exact proof term for the current goal is (andEL (((U ∈ 𝒫 I ∧ V ∈ 𝒫 I) ∧ U ∩ V = Empty) ∧ U ≠ Empty) (V ≠ Empty) Hpart1).
We prove the intermediate claim HVne: V ≠ Empty.
An exact proof term for the current goal is (andER (((U ∈ 𝒫 I ∧ V ∈ 𝒫 I) ∧ U ∩ V = Empty) ∧ U ≠ Empty) (V ≠ Empty) Hpart1).
We prove the intermediate claim Hpowdisj: (U ∈ 𝒫 I ∧ V ∈ 𝒫 I) ∧ U ∩ V = Empty.
An exact proof term for the current goal is (andEL ((U ∈ 𝒫 I ∧ V ∈ 𝒫 I) ∧ U ∩ V = Empty) (U ≠ Empty) HAux).
We prove the intermediate claim HUne: U ≠ Empty.
An exact proof term for the current goal is (andER ((U ∈ 𝒫 I ∧ V ∈ 𝒫 I) ∧ U ∩ V = Empty) (U ≠ Empty) HAux).
We prove the intermediate claim HpowUV: U ∈ 𝒫 I ∧ V ∈ 𝒫 I.
An exact proof term for the current goal is (andEL (U ∈ 𝒫 I ∧ V ∈ 𝒫 I) (U ∩ V = Empty) Hpowdisj).
We prove the intermediate claim HUVdisj: U ∩ V = Empty.
An exact proof term for the current goal is (andER (U ∈ 𝒫 I ∧ V ∈ 𝒫 I) (U ∩ V = Empty) Hpowdisj).
We prove the intermediate claim HUpow: U ∈ 𝒫 I.
An exact proof term for the current goal is (andEL (U ∈ 𝒫 I) (V ∈ 𝒫 I) HpowUV).
We prove the intermediate claim HVpow: V ∈ 𝒫 I.
An exact proof term for the current goal is (andER (U ∈ 𝒫 I) (V ∈ 𝒫 I) HpowUV).
We prove the intermediate claim HTx0: topology_on X Tx0.
An exact proof term for the current goal is (order_topology_is_topology X Hso).
We prove the intermediate claim HISub: I ⊆ X.
Let x be given.
Assume HxI: x ∈ I.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ order_rel X a x0 ∧ order_rel X x0 b) x HxI).
We prove the intermediate claim HIpow: I ∈ 𝒫 X.
An exact proof term for the current goal is (PowerI X I HISub).
Set S1 to be the term {I0 ∈ 𝒫 X|∃a0 ∈ X, ∃b0 ∈ X, I0 = {x ∈ X|order_rel X a0 x ∧ order_rel X x b0}}.
We prove the intermediate claim HIS1: I ∈ S1.
Apply (SepI (𝒫 X) (λI0 : set ⇒ ∃a0 ∈ X, ∃b0 ∈ X, I0 = {x ∈ X|order_rel X a0 x ∧ order_rel X x b0}) I HIpow) 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 HaX.
We use b to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HbX.
Use reflexivity.
Set S2 to be the term {I0 ∈ 𝒫 X|∃b0 ∈ X, I0 = {x ∈ X|order_rel X x b0}}.
Set S3 to be the term {I0 ∈ 𝒫 X|∃a0 ∈ X, I0 = {x ∈ X|order_rel X a0 x}}.
We prove the intermediate claim HIbasis: I ∈ order_topology_basis X.
We prove the intermediate claim HBdef: order_topology_basis X = ((S1 ∪ S2 ∪ S3) ∪ {X}).
Use reflexivity.
rewrite the current goal using HBdef (from left to right).
Apply (binunionI1 (S1 ∪ S2 ∪ S3) {X} I) to the current goal.
Apply (binunionI1 (S1 ∪ S2) S3 I) to the current goal.
Apply (binunionI1 S1 S2 I) to the current goal.
An exact proof term for the current goal is HIS1.
We prove the intermediate claim HIOpen: I ∈ Tx0.
An exact proof term for the current goal is (generated_topology_contains_elem X (order_topology_basis X) I HIpow HIbasis).
We prove the intermediate claim HexU0: ∃U0 ∈ Tx0, U = U0 ∩ I.
An exact proof term for the current goal is (subspace_topologyE X Tx0 I U HUinSub).
Apply HexU0 to the current goal.
Let U0 be given.
Assume HU0pair.
We prove the intermediate claim HU0Tx: U0 ∈ Tx0.
An exact proof term for the current goal is (andEL (U0 ∈ Tx0) (U = U0 ∩ I) HU0pair).
We prove the intermediate claim HUeq: U = U0 ∩ I.
An exact proof term for the current goal is (andER (U0 ∈ Tx0) (U = U0 ∩ I) HU0pair).
We prove the intermediate claim HexV0: ∃V0 ∈ Tx0, V = V0 ∩ I.
An exact proof term for the current goal is (subspace_topologyE X Tx0 I V HVinSub).
Apply HexV0 to the current goal.
Let V0 be given.
Assume HV0pair.
We prove the intermediate claim HV0Tx: V0 ∈ Tx0.
An exact proof term for the current goal is (andEL (V0 ∈ Tx0) (V = V0 ∩ I) HV0pair).
We prove the intermediate claim HVeq: V = V0 ∩ I.
An exact proof term for the current goal is (andER (V0 ∈ Tx0) (V = V0 ∩ I) HV0pair).
We prove the intermediate claim HUopen: U ∈ Tx0.
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is (topology_binintersect_closed X Tx0 U0 I HTx0 HU0Tx HIOpen).
We prove the intermediate claim HVopen: V ∈ Tx0.
rewrite the current goal using HVeq (from left to right).
An exact proof term for the current goal is (topology_binintersect_closed X Tx0 V0 I HTx0 HV0Tx HIOpen).
Apply (nonempty_has_element U HUne) to the current goal.
Let u0 be given.
Assume Hu0U: u0 ∈ U.
Apply (nonempty_has_element V HVne) to the current goal.
Let v0 be given.
Assume Hv0V: v0 ∈ V.
We prove the intermediate claim Hu0I: u0 ∈ I.
An exact proof term for the current goal is ((PowerE I U HUpow) u0 Hu0U).
We prove the intermediate claim Hv0I: v0 ∈ I.
An exact proof term for the current goal is ((PowerE I V HVpow) v0 Hv0V).
We prove the intermediate claim Hu0X: u0 ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ order_rel X a x0 ∧ order_rel X x0 b) u0 Hu0I).
We prove the intermediate claim Hv0X: v0 ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ order_rel X a x0 ∧ order_rel X x0 b) v0 Hv0I).
We prove the intermediate claim Hcomp: order_rel X u0 v0 ∨ order_rel X v0 u0.
Apply (order_rel_trichotomy_or_impred X u0 v0 Hso Hu0X Hv0X (order_rel X u0 v0 ∨ order_rel X v0 u0)) to the current goal.
Assume Huv: order_rel X u0 v0.
Apply orIL to the current goal.
An exact proof term for the current goal is Huv.
Assume Heq: u0 = v0.
Apply FalseE to the current goal.
We prove the intermediate claim Hu0V: u0 ∈ V.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is Hv0V.
We prove the intermediate claim Hu0UV: u0 ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V u0 Hu0U Hu0V).
We prove the intermediate claim HuE: u0 ∈ Empty.
rewrite the current goal using HUVdisj (from right to left).
An exact proof term for the current goal is Hu0UV.
An exact proof term for the current goal is (EmptyE u0 HuE).
Assume Hvu: order_rel X v0 u0.
Apply orIR to the current goal.
An exact proof term for the current goal is Hvu.
Apply Hcomp to the current goal.
Assume Huv: order_rel X u0 v0.
Set A0 to be the term {x ∈ X|x ∈ U ∧ order_rel X x v0}.
We prove the intermediate claim Hu0A0: u0 ∈ A0.
Apply (SepI X (λx0 : set ⇒ x0 ∈ U ∧ order_rel X x0 v0) u0 Hu0X) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hu0U.
An exact proof term for the current goal is Huv.
We prove the intermediate claim HA0ne: A0 ≠ Empty.
An exact proof term for the current goal is (elem_implies_nonempty A0 u0 Hu0A0).
We prove the intermediate claim HA0subX: A0 ⊆ X.
Let x be given.
Assume HxA0: x ∈ A0.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ x0 ∈ U ∧ order_rel X x0 v0) x HxA0).
We prove the intermediate claim Hupper: ∃upper : set, upper ∈ X ∧ ∀a0 : set, a0 ∈ A0 → order_rel X a0 upper ∨ a0 = upper.
We use v0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hv0X.
Let a0 be given.
Assume Ha0A0: a0 ∈ A0.
We prove the intermediate claim Ha0Conj: a0 ∈ U ∧ order_rel X a0 v0.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ x0 ∈ U ∧ order_rel X x0 v0) a0 Ha0A0).
We prove the intermediate claim Ha0v0: order_rel X a0 v0.
An exact proof term for the current goal is (andER (a0 ∈ U) (order_rel X a0 v0) Ha0Conj).
Apply orIL to the current goal.
An exact proof term for the current goal is Ha0v0.
We prove the intermediate claim Hexlub: ∃lub : set, lub ∈ X ∧ (∀a0 : set, a0 ∈ A0 → order_rel X a0 lub ∨ a0 = lub) ∧ (∀bound : set, bound ∈ X → (∀a0 : set, a0 ∈ A0 → order_rel X a0 bound ∨ a0 = bound) → order_rel X lub bound ∨ lub = bound).
An exact proof term for the current goal is (Hlub A0 HA0subX HA0ne Hupper).
Apply Hexlub to the current goal.
Let c be given.
Assume Hcpack.
We prove the intermediate claim HcCore: (c ∈ X ∧ (∀a0 : set, a0 ∈ A0 → order_rel X a0 c ∨ a0 = c)).
An exact proof term for the current goal is (andEL (c ∈ X ∧ (∀a0 : set, a0 ∈ A0 → order_rel X a0 c ∨ a0 = c)) (∀bound : set, bound ∈ X → (∀a0 : set, a0 ∈ A0 → order_rel X a0 bound ∨ a0 = bound) → order_rel X c bound ∨ c = bound) Hcpack).
We prove the intermediate claim HcX: c ∈ X.
An exact proof term for the current goal is (andEL (c ∈ X) (∀a0 : set, a0 ∈ A0 → order_rel X a0 c ∨ a0 = c) HcCore).
We prove the intermediate claim Hcup: ∀a0 : set, a0 ∈ A0 → order_rel X a0 c ∨ a0 = c.
An exact proof term for the current goal is (andER (c ∈ X) (∀a0 : set, a0 ∈ A0 → order_rel X a0 c ∨ a0 = c) HcCore).
We prove the intermediate claim Hcleast: ∀bound : set, bound ∈ X → (∀a0 : set, a0 ∈ A0 → order_rel X a0 bound ∨ a0 = bound) → order_rel X c bound ∨ c = bound.
An exact proof term for the current goal is (andER (c ∈ X ∧ (∀a0 : set, a0 ∈ A0 → order_rel X a0 c ∨ a0 = c)) (∀bound : set, bound ∈ X → (∀a0 : set, a0 ∈ A0 → order_rel X a0 bound ∨ a0 = bound) → order_rel X c bound ∨ c = bound) Hcpack).
We prove the intermediate claim Hau0: order_rel X a u0.
An exact proof term for the current goal is (andEL (order_rel X a u0) (order_rel X u0 b) (SepE2 X (λx0 : set ⇒ order_rel X a x0 ∧ order_rel X x0 b) u0 Hu0I)).
We prove the intermediate claim Hv0b: order_rel X v0 b.
An exact proof term for the current goal is (andER (order_rel X a v0) (order_rel X v0 b) (SepE2 X (λx0 : set ⇒ order_rel X a x0 ∧ order_rel X x0 b) v0 Hv0I)).
We prove the intermediate claim Huv0: order_rel X u0 c ∨ u0 = c.
An exact proof term for the current goal is (Hcup u0 Hu0A0).
We prove the intermediate claim Hac: order_rel X a c.
Apply Huv0 to the current goal.
Assume Hu0c: order_rel X u0 c.
An exact proof term for the current goal is (order_rel_trans X a u0 c Hso HaX Hu0X HcX Hau0 Hu0c).
Assume Hceq: u0 = c.
rewrite the current goal using Hceq (from right to left).
An exact proof term for the current goal is Hau0.
We prove the intermediate claim Hv0Upper: ∀a0 : set, a0 ∈ A0 → order_rel X a0 v0 ∨ a0 = v0.
Let a0 be given.
Assume Ha0A0: a0 ∈ A0.
We prove the intermediate claim Ha0Conj: a0 ∈ U ∧ order_rel X a0 v0.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ x0 ∈ U ∧ order_rel X x0 v0) a0 Ha0A0).
We prove the intermediate claim Ha0v0: order_rel X a0 v0.
An exact proof term for the current goal is (andER (a0 ∈ U) (order_rel X a0 v0) Ha0Conj).
Apply orIL to the current goal.
An exact proof term for the current goal is Ha0v0.
We prove the intermediate claim HcLeV0: order_rel X c v0 ∨ c = v0.
An exact proof term for the current goal is (Hcleast v0 Hv0X Hv0Upper).
We prove the intermediate claim Hcb: order_rel X c b.
Apply HcLeV0 to the current goal.
Assume Hcv0: order_rel X c v0.
An exact proof term for the current goal is (order_rel_trans X c v0 b Hso HcX Hv0X HbX Hcv0 Hv0b).
Assume Hceq: c = v0.
rewrite the current goal using Hceq (from left to right).
An exact proof term for the current goal is Hv0b.
We prove the intermediate claim HcI: c ∈ I.
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ order_rel X a x0 ∧ order_rel X x0 b) c HcX (andI (order_rel X a c) (order_rel X c b) Hac Hcb)).
We prove the intermediate claim HcInUV: c ∈ U ∪ V.
rewrite the current goal using Hunion (from left to right).
An exact proof term for the current goal is HcI.
Apply (binunionE U V c HcInUV) to the current goal.
Assume HcU: c ∈ U.
We prove the intermediate claim HcLtV0: order_rel X c v0.
Apply HcLeV0 to the current goal.
Assume Hcv0: order_rel X c v0.
An exact proof term for the current goal is Hcv0.
Assume Hceq: c = v0.
Apply FalseE to the current goal.
We prove the intermediate claim Hv0U: v0 ∈ U.
rewrite the current goal using Hceq (from right to left).
An exact proof term for the current goal is HcU.
We prove the intermediate claim Hv0UV: v0 ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V v0 Hv0U Hv0V).
We prove the intermediate claim Hv0E: v0 ∈ Empty.
rewrite the current goal using HUVdisj (from right to left).
An exact proof term for the current goal is Hv0UV.
An exact proof term for the current goal is (EmptyE v0 Hv0E).
Set Iv0 to be the term open_ray_lower X v0.
We prove the intermediate claim HIv0B: Iv0 ∈ order_topology_basis X.
An exact proof term for the current goal is (open_ray_lower_in_order_topology_basis X v0 Hv0X).
We prove the intermediate claim HcIv0: c ∈ Iv0.
We prove the intermediate claim HIdef: Iv0 = {x ∈ X|order_rel X x v0}.
Use reflexivity.
rewrite the current goal using HIdef (from left to right).
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ order_rel X x0 v0) c HcX HcLtV0).
We prove the intermediate claim HexB0: ∃B0 ∈ order_topology_basis X, c ∈ B0 ∧ B0 ⊆ U.
An exact proof term for the current goal is (order_topology_local_basis_elem X U c Hso HUopen HcU).
Apply HexB0 to the current goal.
Let B0 be given.
Assume HB0Core.
Apply HB0Core to the current goal.
Assume HB0B HB0Data.
Apply HB0Data to the current goal.
Assume HcB0 HB0subU.
We prove the intermediate claim HBasisOn: basis_on X (order_topology_basis X).
An exact proof term for the current goal is (order_topology_basis_is_basis X Hso).
We prove the intermediate claim HexB3: ∃B3 ∈ order_topology_basis X, c ∈ B3 ∧ B3 ⊆ B0 ∩ Iv0.
An exact proof term for the current goal is (basis_on_refine X (order_topology_basis X) HBasisOn B0 HB0B Iv0 HIv0B c HcB0 HcIv0).
Apply HexB3 to the current goal.
Let B3 be given.
Assume HB3Core.
Apply HB3Core to the current goal.
Assume HB3B HB3Data.
Apply HB3Data to the current goal.
Assume HcB3 HB3Sub.
We prove the intermediate claim Hcases: (∃a0 ∈ X, ∃d ∈ X, B3 = {x ∈ X|order_rel X a0 x ∧ order_rel X x d}) ∨ (∃d ∈ X, B3 = {x ∈ X|order_rel X x d}) ∨ (∃a0 ∈ X, B3 = {x ∈ X|order_rel X a0 x}) ∨ B3 = X.
An exact proof term for the current goal is (order_topology_basis_cases X B3 HB3B).
Apply Hcases to the current goal.
Assume H123: (((∃a0 ∈ X, ∃d ∈ X, B3 = {x ∈ X|order_rel X a0 x ∧ order_rel X x d}) ∨ (∃d ∈ X, B3 = {x ∈ X|order_rel X x d})) ∨ (∃a0 ∈ X, B3 = {x ∈ X|order_rel X a0 x})).
Apply H123 to the current goal.
Assume H12: ((∃a0 ∈ X, ∃d ∈ X, B3 = {x ∈ X|order_rel X a0 x ∧ order_rel X x d}) ∨ (∃d ∈ X, B3 = {x ∈ X|order_rel X x d})).
Apply H12 to the current goal.
Assume HB3I: (∃a0 ∈ X, ∃d ∈ X, B3 = {x ∈ X|order_rel X a0 x ∧ order_rel X x d}).
Apply HB3I to the current goal.
Let a0 be given.
Assume HaCore.
Apply HaCore to the current goal.
Assume Ha0X HdEx.
Apply HdEx to the current goal.
Let d be given.
Assume HdCore.
Apply HdCore to the current goal.
Assume HdX HB3eq.
We prove the intermediate claim HcInI0: c ∈ {x ∈ X|order_rel X a0 x ∧ order_rel X x d}.
rewrite the current goal using HB3eq (from right to left).
An exact proof term for the current goal is HcB3.
We prove the intermediate claim HcProps: order_rel X a0 c ∧ order_rel X c d.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X a0 x0 ∧ order_rel X x0 d) c HcInI0).
We prove the intermediate claim Hcd: order_rel X c d.
An exact proof term for the current goal is (andER (order_rel X a0 c) (order_rel X c d) HcProps).
We prove the intermediate claim Hexz: ∃z : set, z ∈ X ∧ order_rel X c z ∧ order_rel X z d.
An exact proof term for the current goal is (Hbetween c d HcX HdX Hcd).
Apply Hexz to the current goal.
Let z be given.
Assume HzConj.
We prove the intermediate claim HzCore: z ∈ X ∧ order_rel X c z.
An exact proof term for the current goal is (andEL (z ∈ X ∧ order_rel X c z) (order_rel X z d) HzConj).
We prove the intermediate claim HzX: z ∈ X.
An exact proof term for the current goal is (andEL (z ∈ X) (order_rel X c z) HzCore).
We prove the intermediate claim Hcz: order_rel X c z.
An exact proof term for the current goal is (andER (z ∈ X) (order_rel X c z) HzCore).
We prove the intermediate claim HzI0: z ∈ {x ∈ X|order_rel X a0 x ∧ order_rel X x d}.
Apply (SepI X (λx0 : set ⇒ order_rel X a0 x0 ∧ order_rel X x0 d) z HzX) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is (order_rel_trans X a0 c z Hso Ha0X HcX HzX (andEL (order_rel X a0 c) (order_rel X c d) HcProps) Hcz).
An exact proof term for the current goal is (andER (z ∈ X ∧ order_rel X c z) (order_rel X z d) HzConj).
We prove the intermediate claim HzB3: z ∈ B3.
rewrite the current goal using HB3eq (from left to right).
An exact proof term for the current goal is HzI0.
We prove the intermediate claim HzInInter: z ∈ B0 ∩ Iv0.
An exact proof term for the current goal is (HB3Sub z HzB3).
We prove the intermediate claim HzB0: z ∈ B0.
An exact proof term for the current goal is (binintersectE1 B0 Iv0 z HzInInter).
We prove the intermediate claim HzIv0: z ∈ Iv0.
An exact proof term for the current goal is (binintersectE2 B0 Iv0 z HzInInter).
We prove the intermediate claim HzU: z ∈ U.
An exact proof term for the current goal is (HB0subU z HzB0).
We prove the intermediate claim Hzltv0: order_rel X z v0.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X x0 v0) z HzIv0).
We prove the intermediate claim HzA0: z ∈ A0.
Apply (SepI X (λx0 : set ⇒ x0 ∈ U ∧ order_rel X x0 v0) z HzX) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HzU.
An exact proof term for the current goal is Hzltv0.
Apply (Hcup z HzA0) to the current goal.
Assume Hzltc: order_rel X z c.
We prove the intermediate claim Hcc: order_rel X c c.
An exact proof term for the current goal is (order_rel_trans X c z c Hso HcX HzX HcX Hcz Hzltc).
An exact proof term for the current goal is ((order_rel_irref X c) Hcc).
Assume Hzeq: z = c.
We prove the intermediate claim Hcc: order_rel X c c.
rewrite the current goal using Hzeq (from right to left) at position 2.
An exact proof term for the current goal is Hcz.
An exact proof term for the current goal is ((order_rel_irref X c) Hcc).
Assume HB3L: (∃d ∈ X, B3 = {x ∈ X|order_rel X x d}).
Apply HB3L to the current goal.
Let d be given.
Assume HdCore.
Apply HdCore to the current goal.
Assume HdX HB3eq.
We prove the intermediate claim HcInL: c ∈ {x ∈ X|order_rel X x d}.
rewrite the current goal using HB3eq (from right to left).
An exact proof term for the current goal is HcB3.
We prove the intermediate claim Hcd: order_rel X c d.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X x0 d) c HcInL).
We prove the intermediate claim Hexz: ∃z : set, z ∈ X ∧ order_rel X c z ∧ order_rel X z d.
An exact proof term for the current goal is (Hbetween c d HcX HdX Hcd).
Apply Hexz to the current goal.
Let z be given.
Assume HzConj.
We prove the intermediate claim HzCore: z ∈ X ∧ order_rel X c z.
An exact proof term for the current goal is (andEL (z ∈ X ∧ order_rel X c z) (order_rel X z d) HzConj).
We prove the intermediate claim HzX: z ∈ X.
An exact proof term for the current goal is (andEL (z ∈ X) (order_rel X c z) HzCore).
We prove the intermediate claim Hcz: order_rel X c z.
An exact proof term for the current goal is (andER (z ∈ X) (order_rel X c z) HzCore).
We prove the intermediate claim Hzld: order_rel X z d.
An exact proof term for the current goal is (andER (z ∈ X ∧ order_rel X c z) (order_rel X z d) HzConj).
We prove the intermediate claim HzL: z ∈ {x ∈ X|order_rel X x d}.
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ order_rel X x0 d) z HzX Hzld).
We prove the intermediate claim HzB3: z ∈ B3.
rewrite the current goal using HB3eq (from left to right).
An exact proof term for the current goal is HzL.
We prove the intermediate claim HzInInter: z ∈ B0 ∩ Iv0.
An exact proof term for the current goal is (HB3Sub z HzB3).
We prove the intermediate claim HzB0: z ∈ B0.
An exact proof term for the current goal is (binintersectE1 B0 Iv0 z HzInInter).
We prove the intermediate claim HzIv0: z ∈ Iv0.
An exact proof term for the current goal is (binintersectE2 B0 Iv0 z HzInInter).
We prove the intermediate claim HzU: z ∈ U.
An exact proof term for the current goal is (HB0subU z HzB0).
We prove the intermediate claim Hzltv0: order_rel X z v0.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X x0 v0) z HzIv0).
We prove the intermediate claim HzA0: z ∈ A0.
Apply (SepI X (λx0 : set ⇒ x0 ∈ U ∧ order_rel X x0 v0) z HzX) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HzU.
An exact proof term for the current goal is Hzltv0.
Apply (Hcup z HzA0) to the current goal.
Assume Hzltc: order_rel X z c.
We prove the intermediate claim Hcc: order_rel X c c.
An exact proof term for the current goal is (order_rel_trans X c z c Hso HcX HzX HcX Hcz Hzltc).
An exact proof term for the current goal is ((order_rel_irref X c) Hcc).
Assume Hzeq: z = c.
We prove the intermediate claim Hcc: order_rel X c c.
rewrite the current goal using Hzeq (from right to left) at position 2.
An exact proof term for the current goal is Hcz.
An exact proof term for the current goal is ((order_rel_irref X c) Hcc).
Assume HB3R: (∃a0 ∈ X, B3 = {x ∈ X|order_rel X a0 x}).
Apply HB3R to the current goal.
Let a0 be given.
Assume HaCore.
Apply HaCore to the current goal.
Assume Ha0X HB3eq.
We prove the intermediate claim HcInR: c ∈ {x ∈ X|order_rel X a0 x}.
rewrite the current goal using HB3eq (from right to left).
An exact proof term for the current goal is HcB3.
We prove the intermediate claim Hac0: order_rel X a0 c.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X a0 x0) c HcInR).
We prove the intermediate claim Hav0: order_rel X a0 v0.
An exact proof term for the current goal is (order_rel_trans X a0 c v0 Hso Ha0X HcX Hv0X Hac0 HcLtV0).
We prove the intermediate claim Hv0B3: v0 ∈ B3.
rewrite the current goal using HB3eq (from left to right).
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ order_rel X a0 x0) v0 Hv0X Hav0).
We prove the intermediate claim Hv0InInter: v0 ∈ B0 ∩ Iv0.
An exact proof term for the current goal is (HB3Sub v0 Hv0B3).
We prove the intermediate claim Hv0Iv0: v0 ∈ Iv0.
An exact proof term for the current goal is (binintersectE2 B0 Iv0 v0 Hv0InInter).
We prove the intermediate claim Hv0ltv0: order_rel X v0 v0.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X x0 v0) v0 Hv0Iv0).
An exact proof term for the current goal is ((order_rel_irref X v0) Hv0ltv0).
Assume HB3X: B3 = X.
We prove the intermediate claim Hv0B3: v0 ∈ B3.
rewrite the current goal using HB3X (from left to right).
An exact proof term for the current goal is Hv0X.
We prove the intermediate claim Hv0InInter: v0 ∈ B0 ∩ Iv0.
An exact proof term for the current goal is (HB3Sub v0 Hv0B3).
We prove the intermediate claim Hv0Iv0: v0 ∈ Iv0.
An exact proof term for the current goal is (binintersectE2 B0 Iv0 v0 Hv0InInter).
We prove the intermediate claim Hv0ltv0: order_rel X v0 v0.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X x0 v0) v0 Hv0Iv0).
An exact proof term for the current goal is ((order_rel_irref X v0) Hv0ltv0).
Assume HcV: c ∈ V.
We prove the intermediate claim HcnotU: ¬ (c ∈ U).
Assume HcU2: c ∈ U.
We prove the intermediate claim HcUV: c ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V c HcU2 HcV).
We prove the intermediate claim HcE: c ∈ Empty.
rewrite the current goal using HUVdisj (from right to left).
An exact proof term for the current goal is HcUV.
An exact proof term for the current goal is (EmptyE c HcE).
We prove the intermediate claim Hcup_lt: ∀a0 : set, a0 ∈ A0 → order_rel X a0 c.
Let a0 be given.
Assume Ha0A0: a0 ∈ A0.
Apply (Hcup a0 Ha0A0) to the current goal.
Assume Hac0: order_rel X a0 c.
An exact proof term for the current goal is Hac0.
Assume Haeq: a0 = c.
Apply FalseE to the current goal.
We prove the intermediate claim HcA0: c ∈ A0.
rewrite the current goal using Haeq (from right to left).
An exact proof term for the current goal is Ha0A0.
We prove the intermediate claim HcConj: c ∈ U ∧ order_rel X c v0.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ x0 ∈ U ∧ order_rel X x0 v0) c HcA0).
We prove the intermediate claim HcU2: c ∈ U.
An exact proof term for the current goal is (andEL (c ∈ U) (order_rel X c v0) HcConj).
An exact proof term for the current goal is (HcnotU HcU2).
We prove the intermediate claim HexBv: ∃Bv ∈ order_topology_basis X, c ∈ Bv ∧ Bv ⊆ V.
An exact proof term for the current goal is (order_topology_local_basis_elem X V c Hso HVopen HcV).
Apply HexBv to the current goal.
Let Bv be given.
Assume HBvCore.
Apply HBvCore to the current goal.
Assume HBvB HBvData.
Apply HBvData to the current goal.
Assume HcBv HBvsubV.
We prove the intermediate claim HcasesBv: (∃l ∈ X, ∃r ∈ X, Bv = {x ∈ X|order_rel X l x ∧ order_rel X x r}) ∨ (∃r ∈ X, Bv = {x ∈ X|order_rel X x r}) ∨ (∃l ∈ X, Bv = {x ∈ X|order_rel X l x}) ∨ Bv = X.
An exact proof term for the current goal is (order_topology_basis_cases X Bv HBvB).
Apply HcasesBv to the current goal.
Assume H123Bv: (((∃l ∈ X, ∃r ∈ X, Bv = {x ∈ X|order_rel X l x ∧ order_rel X x r}) ∨ (∃r ∈ X, Bv = {x ∈ X|order_rel X x r})) ∨ (∃l ∈ X, Bv = {x ∈ X|order_rel X l x})).
Apply H123Bv to the current goal.
Assume H12Bv: ((∃l ∈ X, ∃r ∈ X, Bv = {x ∈ X|order_rel X l x ∧ order_rel X x r}) ∨ (∃r ∈ X, Bv = {x ∈ X|order_rel X x r})).
Apply H12Bv to the current goal.
Assume HBvI: (∃l ∈ X, ∃r ∈ X, Bv = {x ∈ X|order_rel X l x ∧ order_rel X x r}).
Apply HBvI to the current goal.
Let l be given.
Assume HlCore.
Apply HlCore to the current goal.
Assume HlX HrEx.
Apply HrEx to the current goal.
Let r be given.
Assume HrCore.
Apply HrCore to the current goal.
Assume HrX HBveq.
We prove the intermediate claim HcInI0: c ∈ {x ∈ X|order_rel X l x ∧ order_rel X x r}.
rewrite the current goal using HBveq (from right to left).
An exact proof term for the current goal is HcBv.
We prove the intermediate claim HcProps: order_rel X l c ∧ order_rel X c r.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X l x0 ∧ order_rel X x0 r) c HcInI0).
We prove the intermediate claim Hlc: order_rel X l c.
An exact proof term for the current goal is (andEL (order_rel X l c) (order_rel X c r) HcProps).
We prove the intermediate claim Hcr: order_rel X c r.
An exact proof term for the current goal is (andER (order_rel X l c) (order_rel X c r) HcProps).
We prove the intermediate claim HcontraUB: ¬ (∀x : set, x ∈ A0 → order_rel X x l ∨ x = l).
Assume Hub: ∀x : set, x ∈ A0 → order_rel X x l ∨ x = l.
We prove the intermediate claim Hcl: order_rel X c l ∨ c = l.
An exact proof term for the current goal is (Hcleast l HlX Hub).
Apply Hcl to the current goal.
Assume HclRel: order_rel X c l.
We prove the intermediate claim Hll: order_rel X l l.
An exact proof term for the current goal is (order_rel_trans X l c l Hso HlX HcX HlX Hlc HclRel).
An exact proof term for the current goal is ((order_rel_irref X l) Hll).
Assume Hceq: c = l.
We prove the intermediate claim Hll: order_rel X l l.
rewrite the current goal using Hceq (from right to left) at position 2.
An exact proof term for the current goal is Hlc.
An exact proof term for the current goal is ((order_rel_irref X l) Hll).
We prove the intermediate claim Hexnl: ∃x : set, ¬ (x ∈ A0 → order_rel X x l ∨ x = l).
An exact proof term for the current goal is (not_all_ex_demorgan_i (λx : set ⇒ x ∈ A0 → order_rel X x l ∨ x = l) HcontraUB).
Apply Hexnl to the current goal.
Let x be given.
Assume HnotImp: ¬ (x ∈ A0 → order_rel X x l ∨ x = l).
We prove the intermediate claim HxA0_and: x ∈ A0 ∧ ¬ (order_rel X x l ∨ x = l).
An exact proof term for the current goal is (not_imp (x ∈ A0) (order_rel X x l ∨ x = l) HnotImp).
We prove the intermediate claim HxA0: x ∈ A0.
An exact proof term for the current goal is (andEL (x ∈ A0) (¬ (order_rel X x l ∨ x = l)) HxA0_and).
We prove the intermediate claim Hxnotle: ¬ (order_rel X x l ∨ x = l).
An exact proof term for the current goal is (andER (x ∈ A0) (¬ (order_rel X x l ∨ x = l)) HxA0_and).
We prove the intermediate claim Hxnot: ¬ (order_rel X x l) ∧ x ≠ l.
An exact proof term for the current goal is (not_or_and_demorgan (order_rel X x l) (x = l) Hxnotle).
We prove the intermediate claim Hxnotxl: ¬ (order_rel X x l).
An exact proof term for the current goal is (andEL (¬ (order_rel X x l)) (¬ (x = l)) Hxnot).
We prove the intermediate claim Hxneq: x ≠ l.
An exact proof term for the current goal is (andER (¬ (order_rel X x l)) (¬ (x = l)) Hxnot).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ x0 ∈ U ∧ order_rel X x0 v0) x HxA0).
We prove the intermediate claim Hxl: order_rel X l x.
Apply (order_rel_trichotomy_or_impred X l x Hso HlX HxX (order_rel X l x)) to the current goal.
Assume Hlx: order_rel X l x.
An exact proof term for the current goal is Hlx.
Assume Heq: l = x.
Apply FalseE to the current goal.
Apply Hxneq to the current goal.
Use symmetry.
An exact proof term for the current goal is Heq.
Assume Hxlt: order_rel X x l.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hxnotxl Hxlt).
We prove the intermediate claim Hxc: order_rel X x c.
An exact proof term for the current goal is (Hcup_lt x HxA0).
We prove the intermediate claim Hxr: order_rel X x r.
An exact proof term for the current goal is (order_rel_trans X x c r Hso HxX HcX HrX Hxc Hcr).
We prove the intermediate claim HxI0: x ∈ {x0 ∈ X|order_rel X l x0 ∧ order_rel X x0 r}.
Apply (SepI X (λx0 : set ⇒ order_rel X l x0 ∧ order_rel X x0 r) x HxX) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hxl.
An exact proof term for the current goal is Hxr.
We prove the intermediate claim HxBv: x ∈ Bv.
rewrite the current goal using HBveq (from left to right).
An exact proof term for the current goal is HxI0.
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (HBvsubV x HxBv).
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (andEL (x ∈ U) (order_rel X x v0) (SepE2 X (λx0 : set ⇒ x0 ∈ U ∧ order_rel X x0 v0) x HxA0)).
We prove the intermediate claim HxUV: x ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V x HxU HxV).
We prove the intermediate claim HxE: x ∈ Empty.
rewrite the current goal using HUVdisj (from right to left).
An exact proof term for the current goal is HxUV.
An exact proof term for the current goal is (EmptyE x HxE).
Assume HBvL: (∃r ∈ X, Bv = {x ∈ X|order_rel X x r}).
Apply HBvL to the current goal.
Let r be given.
Assume HrCore.
Apply HrCore to the current goal.
Assume HrX HBveq.
We prove the intermediate claim HcInL0: c ∈ {x ∈ X|order_rel X x r}.
rewrite the current goal using HBveq (from right to left).
An exact proof term for the current goal is HcBv.
We prove the intermediate claim Hcr: order_rel X c r.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X x0 r) c HcInL0).
We prove the intermediate claim Hu0c: order_rel X u0 c.
An exact proof term for the current goal is (Hcup_lt u0 Hu0A0).
We prove the intermediate claim Hu0r: order_rel X u0 r.
An exact proof term for the current goal is (order_rel_trans X u0 c r Hso Hu0X HcX HrX Hu0c Hcr).
We prove the intermediate claim Hu0L0: u0 ∈ {x0 ∈ X|order_rel X x0 r}.
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ order_rel X x0 r) u0 Hu0X Hu0r).
We prove the intermediate claim Hu0Bv: u0 ∈ Bv.
rewrite the current goal using HBveq (from left to right).
An exact proof term for the current goal is Hu0L0.
We prove the intermediate claim Hu0V2: u0 ∈ V.
An exact proof term for the current goal is (HBvsubV u0 Hu0Bv).
We prove the intermediate claim Hu0UV: u0 ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V u0 Hu0U Hu0V2).
We prove the intermediate claim Hu0E: u0 ∈ Empty.
rewrite the current goal using HUVdisj (from right to left).
An exact proof term for the current goal is Hu0UV.
An exact proof term for the current goal is (EmptyE u0 Hu0E).
Assume HBvR: (∃l ∈ X, Bv = {x ∈ X|order_rel X l x}).
Apply HBvR to the current goal.
Let l be given.
Assume HlCore.
Apply HlCore to the current goal.
Assume HlX HBveq.
We prove the intermediate claim HcInR0: c ∈ {x ∈ X|order_rel X l x}.
rewrite the current goal using HBveq (from right to left).
An exact proof term for the current goal is HcBv.
We prove the intermediate claim Hlc: order_rel X l c.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X l x0) c HcInR0).
We prove the intermediate claim HcontraUB: ¬ (∀x : set, x ∈ A0 → order_rel X x l ∨ x = l).
Assume Hub: ∀x : set, x ∈ A0 → order_rel X x l ∨ x = l.
We prove the intermediate claim Hcl: order_rel X c l ∨ c = l.
An exact proof term for the current goal is (Hcleast l HlX Hub).
Apply Hcl to the current goal.
Assume HclRel: order_rel X c l.
We prove the intermediate claim Hll: order_rel X l l.
An exact proof term for the current goal is (order_rel_trans X l c l Hso HlX HcX HlX Hlc HclRel).
An exact proof term for the current goal is ((order_rel_irref X l) Hll).
Assume Hceq: c = l.
We prove the intermediate claim Hll: order_rel X l l.
rewrite the current goal using Hceq (from right to left) at position 2.
An exact proof term for the current goal is Hlc.
An exact proof term for the current goal is ((order_rel_irref X l) Hll).
We prove the intermediate claim Hexnl: ∃x : set, ¬ (x ∈ A0 → order_rel X x l ∨ x = l).
An exact proof term for the current goal is (not_all_ex_demorgan_i (λx : set ⇒ x ∈ A0 → order_rel X x l ∨ x = l) HcontraUB).
Apply Hexnl to the current goal.
Let x be given.
Assume HnotImp: ¬ (x ∈ A0 → order_rel X x l ∨ x = l).
We prove the intermediate claim HxA0_and: x ∈ A0 ∧ ¬ (order_rel X x l ∨ x = l).
An exact proof term for the current goal is (not_imp (x ∈ A0) (order_rel X x l ∨ x = l) HnotImp).
We prove the intermediate claim HxA0: x ∈ A0.
An exact proof term for the current goal is (andEL (x ∈ A0) (¬ (order_rel X x l ∨ x = l)) HxA0_and).
We prove the intermediate claim Hxnotle: ¬ (order_rel X x l ∨ x = l).
An exact proof term for the current goal is (andER (x ∈ A0) (¬ (order_rel X x l ∨ x = l)) HxA0_and).
We prove the intermediate claim Hxnot: ¬ (order_rel X x l) ∧ x ≠ l.
An exact proof term for the current goal is (not_or_and_demorgan (order_rel X x l) (x = l) Hxnotle).
We prove the intermediate claim Hxnotxl: ¬ (order_rel X x l).
An exact proof term for the current goal is (andEL (¬ (order_rel X x l)) (¬ (x = l)) Hxnot).
We prove the intermediate claim Hxneq: x ≠ l.
An exact proof term for the current goal is (andER (¬ (order_rel X x l)) (¬ (x = l)) Hxnot).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ x0 ∈ U ∧ order_rel X x0 v0) x HxA0).
We prove the intermediate claim Hxl: order_rel X l x.
Apply (order_rel_trichotomy_or_impred X l x Hso HlX HxX (order_rel X l x)) to the current goal.
Assume Hlx: order_rel X l x.
An exact proof term for the current goal is Hlx.
Assume Heq: l = x.
Apply FalseE to the current goal.
Apply Hxneq to the current goal.
Use symmetry.
An exact proof term for the current goal is Heq.
Assume Hxlt: order_rel X x l.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hxnotxl Hxlt).
We prove the intermediate claim HxBv: x ∈ Bv.
rewrite the current goal using HBveq (from left to right).
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ order_rel X l x0) x HxX Hxl).
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (HBvsubV x HxBv).
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (andEL (x ∈ U) (order_rel X x v0) (SepE2 X (λx0 : set ⇒ x0 ∈ U ∧ order_rel X x0 v0) x HxA0)).
We prove the intermediate claim HxUV: x ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V x HxU HxV).
We prove the intermediate claim HxE: x ∈ Empty.
rewrite the current goal using HUVdisj (from right to left).
An exact proof term for the current goal is HxUV.
An exact proof term for the current goal is (EmptyE x HxE).
Assume HBvX: Bv = X.
We prove the intermediate claim Hu0V2: u0 ∈ V.
Apply HBvsubV to the current goal.
rewrite the current goal using HBvX (from left to right).
An exact proof term for the current goal is Hu0X.
We prove the intermediate claim Hu0UV: u0 ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V u0 Hu0U Hu0V2).
We prove the intermediate claim Hu0E: u0 ∈ Empty.
rewrite the current goal using HUVdisj (from right to left).
An exact proof term for the current goal is Hu0UV.
An exact proof term for the current goal is (EmptyE u0 Hu0E).
Assume Hvu: order_rel X v0 u0.
Set A1 to be the term {x ∈ X|x ∈ V ∧ order_rel X x u0}.
We prove the intermediate claim HA1subX: A1 ⊆ X.
Let x be given.
Assume HxA1: x ∈ A1.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ x0 ∈ V ∧ order_rel X x0 u0) x HxA1).
We prove the intermediate claim Hv0A1: v0 ∈ A1.
Apply (SepI X (λx0 : set ⇒ x0 ∈ V ∧ order_rel X x0 u0) v0 Hv0X) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hv0V.
An exact proof term for the current goal is Hvu.
We prove the intermediate claim HA1ne: A1 ≠ Empty.
An exact proof term for the current goal is (elem_implies_nonempty A1 v0 Hv0A1).
We prove the intermediate claim Hupper1: ∃upper : set, upper ∈ X ∧ ∀a0 : set, a0 ∈ A1 → order_rel X a0 upper ∨ a0 = upper.
We use u0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hu0X.
Let a0 be given.
Assume Ha0A1: a0 ∈ A1.
We prove the intermediate claim Ha0Conj: a0 ∈ V ∧ order_rel X a0 u0.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ x0 ∈ V ∧ order_rel X x0 u0) a0 Ha0A1).
We prove the intermediate claim Hau0: order_rel X a0 u0.
An exact proof term for the current goal is (andER (a0 ∈ V) (order_rel X a0 u0) Ha0Conj).
Apply orIL to the current goal.
An exact proof term for the current goal is Hau0.
We prove the intermediate claim Hexlub1: ∃lub : set, lub ∈ X ∧ (∀a0 : set, a0 ∈ A1 → order_rel X a0 lub ∨ a0 = lub) ∧ (∀bound : set, bound ∈ X → (∀a0 : set, a0 ∈ A1 → order_rel X a0 bound ∨ a0 = bound) → order_rel X lub bound ∨ lub = bound).
An exact proof term for the current goal is (Hlub A1 HA1subX HA1ne Hupper1).
Apply Hexlub1 to the current goal.
Let c1 be given.
Assume Hc1pack.
We prove the intermediate claim Hc1Core: (c1 ∈ X ∧ (∀a0 : set, a0 ∈ A1 → order_rel X a0 c1 ∨ a0 = c1)).
An exact proof term for the current goal is (andEL (c1 ∈ X ∧ (∀a0 : set, a0 ∈ A1 → order_rel X a0 c1 ∨ a0 = c1)) (∀bound : set, bound ∈ X → (∀a0 : set, a0 ∈ A1 → order_rel X a0 bound ∨ a0 = bound) → order_rel X c1 bound ∨ c1 = bound) Hc1pack).
We prove the intermediate claim Hc1X: c1 ∈ X.
An exact proof term for the current goal is (andEL (c1 ∈ X) (∀a0 : set, a0 ∈ A1 → order_rel X a0 c1 ∨ a0 = c1) Hc1Core).
We prove the intermediate claim Hcup1: ∀a0 : set, a0 ∈ A1 → order_rel X a0 c1 ∨ a0 = c1.
An exact proof term for the current goal is (andER (c1 ∈ X) (∀a0 : set, a0 ∈ A1 → order_rel X a0 c1 ∨ a0 = c1) Hc1Core).
We prove the intermediate claim Hcleast1: ∀bound : set, bound ∈ X → (∀a0 : set, a0 ∈ A1 → order_rel X a0 bound ∨ a0 = bound) → order_rel X c1 bound ∨ c1 = bound.
An exact proof term for the current goal is (andER (c1 ∈ X ∧ (∀a0 : set, a0 ∈ A1 → order_rel X a0 c1 ∨ a0 = c1)) (∀bound : set, bound ∈ X → (∀a0 : set, a0 ∈ A1 → order_rel X a0 bound ∨ a0 = bound) → order_rel X c1 bound ∨ c1 = bound) Hc1pack).
We prove the intermediate claim Hav0: order_rel X a v0.
An exact proof term for the current goal is (andEL (order_rel X a v0) (order_rel X v0 b) (SepE2 X (λx0 : set ⇒ order_rel X a x0 ∧ order_rel X x0 b) v0 Hv0I)).
We prove the intermediate claim Hu0b: order_rel X u0 b.
An exact proof term for the current goal is (andER (order_rel X a u0) (order_rel X u0 b) (SepE2 X (λx0 : set ⇒ order_rel X a x0 ∧ order_rel X x0 b) u0 Hu0I)).
We prove the intermediate claim Hv0LeC1: order_rel X v0 c1 ∨ v0 = c1.
An exact proof term for the current goal is (Hcup1 v0 Hv0A1).
We prove the intermediate claim Hac1: order_rel X a c1.
Apply Hv0LeC1 to the current goal.
Assume Hv0c1: order_rel X v0 c1.
An exact proof term for the current goal is (order_rel_trans X a v0 c1 Hso HaX Hv0X Hc1X Hav0 Hv0c1).
Assume Hceq: v0 = c1.
rewrite the current goal using Hceq (from right to left).
An exact proof term for the current goal is Hav0.
We prove the intermediate claim Hu0Upper: ∀a0 : set, a0 ∈ A1 → order_rel X a0 u0 ∨ a0 = u0.
Let a0 be given.
Assume Ha0A1: a0 ∈ A1.
We prove the intermediate claim Ha0Conj: a0 ∈ V ∧ order_rel X a0 u0.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ x0 ∈ V ∧ order_rel X x0 u0) a0 Ha0A1).
We prove the intermediate claim Hau0: order_rel X a0 u0.
An exact proof term for the current goal is (andER (a0 ∈ V) (order_rel X a0 u0) Ha0Conj).
Apply orIL to the current goal.
An exact proof term for the current goal is Hau0.
We prove the intermediate claim Hc1LeU0: order_rel X c1 u0 ∨ c1 = u0.
An exact proof term for the current goal is (Hcleast1 u0 Hu0X Hu0Upper).
We prove the intermediate claim Hc1b: order_rel X c1 b.
Apply Hc1LeU0 to the current goal.
Assume Hc1u0: order_rel X c1 u0.
An exact proof term for the current goal is (order_rel_trans X c1 u0 b Hso Hc1X Hu0X HbX Hc1u0 Hu0b).
Assume Hceq: c1 = u0.
rewrite the current goal using Hceq (from left to right).
An exact proof term for the current goal is Hu0b.
We prove the intermediate claim Hc1I: c1 ∈ I.
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ order_rel X a x0 ∧ order_rel X x0 b) c1 Hc1X (andI (order_rel X a c1) (order_rel X c1 b) Hac1 Hc1b)).
We prove the intermediate claim Hc1InUV: c1 ∈ U ∪ V.
rewrite the current goal using Hunion (from left to right).
An exact proof term for the current goal is Hc1I.
Apply (binunionE U V c1 Hc1InUV) to the current goal.
Assume Hc1U: c1 ∈ U.
We prove the intermediate claim Hc1notV: ¬ (c1 ∈ V).
Assume Hc1V2: c1 ∈ V.
We prove the intermediate claim Hc1UV: c1 ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V c1 Hc1U Hc1V2).
We prove the intermediate claim Hc1E: c1 ∈ Empty.
rewrite the current goal using HUVdisj (from right to left).
An exact proof term for the current goal is Hc1UV.
An exact proof term for the current goal is (EmptyE c1 Hc1E).
We prove the intermediate claim Hcup1_lt: ∀a0 : set, a0 ∈ A1 → order_rel X a0 c1.
Let a0 be given.
Assume Ha0A1: a0 ∈ A1.
Apply (Hcup1 a0 Ha0A1) to the current goal.
Assume Ha0c1: order_rel X a0 c1.
An exact proof term for the current goal is Ha0c1.
Assume Ha0eq: a0 = c1.
Apply FalseE to the current goal.
We prove the intermediate claim Hc1A1: c1 ∈ A1.
rewrite the current goal using Ha0eq (from right to left).
An exact proof term for the current goal is Ha0A1.
We prove the intermediate claim Hc1Conj: c1 ∈ V ∧ order_rel X c1 u0.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ x0 ∈ V ∧ order_rel X x0 u0) c1 Hc1A1).
We prove the intermediate claim Hc1V2: c1 ∈ V.
An exact proof term for the current goal is (andEL (c1 ∈ V) (order_rel X c1 u0) Hc1Conj).
An exact proof term for the current goal is (Hc1notV Hc1V2).
We prove the intermediate claim HexbU: ∃b0 ∈ order_topology_basis X, c1 ∈ b0 ∧ b0 ⊆ U.
An exact proof term for the current goal is (order_topology_local_basis_elem X U c1 Hso HUopen Hc1U).
Apply HexbU to the current goal.
Let b0 be given.
Assume Hb0Core.
Apply Hb0Core to the current goal.
Assume Hb0B Hb0Data.
Apply Hb0Data to the current goal.
Assume Hc1b0 Hb0subU.
We prove the intermediate claim Hcasesb: (∃a0 ∈ X, ∃d ∈ X, b0 = {x ∈ X|order_rel X a0 x ∧ order_rel X x d}) ∨ (∃d ∈ X, b0 = {x ∈ X|order_rel X x d}) ∨ (∃a0 ∈ X, b0 = {x ∈ X|order_rel X a0 x}) ∨ b0 = X.
An exact proof term for the current goal is (order_topology_basis_cases X b0 Hb0B).
Apply Hcasesb to the current goal.
Assume H123b: (((∃a0 ∈ X, ∃d ∈ X, b0 = {x ∈ X|order_rel X a0 x ∧ order_rel X x d}) ∨ (∃d ∈ X, b0 = {x ∈ X|order_rel X x d})) ∨ (∃a0 ∈ X, b0 = {x ∈ X|order_rel X a0 x})).
Apply H123b to the current goal.
Assume H12b: ((∃a0 ∈ X, ∃d ∈ X, b0 = {x ∈ X|order_rel X a0 x ∧ order_rel X x d}) ∨ (∃d ∈ X, b0 = {x ∈ X|order_rel X x d})).
Apply H12b to the current goal.
Assume Hb0I: (∃a0 ∈ X, ∃d ∈ X, b0 = {x ∈ X|order_rel X a0 x ∧ order_rel X x d}).
Apply Hb0I to the current goal.
Let a0 be given.
Assume HaCore.
Apply HaCore to the current goal.
Assume Ha0X HdEx.
Apply HdEx to the current goal.
Let d be given.
Assume HdCore.
Apply HdCore to the current goal.
Assume HdX Hb0eq.
We prove the intermediate claim Hc1InI0: c1 ∈ {x ∈ X|order_rel X a0 x ∧ order_rel X x d}.
rewrite the current goal using Hb0eq (from right to left).
An exact proof term for the current goal is Hc1b0.
We prove the intermediate claim Hc1Props: order_rel X a0 c1 ∧ order_rel X c1 d.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X a0 x0 ∧ order_rel X x0 d) c1 Hc1InI0).
We prove the intermediate claim Ha0c1: order_rel X a0 c1.
An exact proof term for the current goal is (andEL (order_rel X a0 c1) (order_rel X c1 d) Hc1Props).
We prove the intermediate claim Hc1d: order_rel X c1 d.
An exact proof term for the current goal is (andER (order_rel X a0 c1) (order_rel X c1 d) Hc1Props).
We prove the intermediate claim HcontraUB: ¬ (∀x : set, x ∈ A1 → order_rel X x a0 ∨ x = a0).
Assume Hub: ∀x : set, x ∈ A1 → order_rel X x a0 ∨ x = a0.
We prove the intermediate claim Hc1a0: order_rel X c1 a0 ∨ c1 = a0.
An exact proof term for the current goal is (Hcleast1 a0 Ha0X Hub).
Apply Hc1a0 to the current goal.
Assume Hc1a0Rel: order_rel X c1 a0.
We prove the intermediate claim Ha0a0: order_rel X a0 a0.
An exact proof term for the current goal is (order_rel_trans X a0 c1 a0 Hso Ha0X Hc1X Ha0X Ha0c1 Hc1a0Rel).
An exact proof term for the current goal is ((order_rel_irref X a0) Ha0a0).
Assume Hc1eq: c1 = a0.
We prove the intermediate claim Ha0a0: order_rel X a0 a0.
rewrite the current goal using Hc1eq (from right to left) at position 2.
An exact proof term for the current goal is Ha0c1.
An exact proof term for the current goal is ((order_rel_irref X a0) Ha0a0).
We prove the intermediate claim Hexna: ∃x : set, ¬ (x ∈ A1 → order_rel X x a0 ∨ x = a0).
An exact proof term for the current goal is (not_all_ex_demorgan_i (λx : set ⇒ x ∈ A1 → order_rel X x a0 ∨ x = a0) HcontraUB).
Apply Hexna to the current goal.
Let x be given.
Assume HnotImp: ¬ (x ∈ A1 → order_rel X x a0 ∨ x = a0).
We prove the intermediate claim HxA1_and: x ∈ A1 ∧ ¬ (order_rel X x a0 ∨ x = a0).
An exact proof term for the current goal is (not_imp (x ∈ A1) (order_rel X x a0 ∨ x = a0) HnotImp).
We prove the intermediate claim HxA1: x ∈ A1.
An exact proof term for the current goal is (andEL (x ∈ A1) (¬ (order_rel X x a0 ∨ x = a0)) HxA1_and).
We prove the intermediate claim Hxnotle: ¬ (order_rel X x a0 ∨ x = a0).
An exact proof term for the current goal is (andER (x ∈ A1) (¬ (order_rel X x a0 ∨ x = a0)) HxA1_and).
We prove the intermediate claim Hxnot: ¬ (order_rel X x a0) ∧ x ≠ a0.
An exact proof term for the current goal is (not_or_and_demorgan (order_rel X x a0) (x = a0) Hxnotle).
We prove the intermediate claim Hxnotxa: ¬ (order_rel X x a0).
An exact proof term for the current goal is (andEL (¬ (order_rel X x a0)) (¬ (x = a0)) Hxnot).
We prove the intermediate claim Hxneq: x ≠ a0.
An exact proof term for the current goal is (andER (¬ (order_rel X x a0)) (¬ (x = a0)) Hxnot).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ x0 ∈ V ∧ order_rel X x0 u0) x HxA1).
We prove the intermediate claim Hxa0: order_rel X a0 x.
Apply (order_rel_trichotomy_or_impred X a0 x Hso Ha0X HxX (order_rel X a0 x)) to the current goal.
Assume Ha0x: order_rel X a0 x.
An exact proof term for the current goal is Ha0x.
Assume Heq: a0 = x.
Apply FalseE to the current goal.
Apply Hxneq to the current goal.
Use symmetry.
An exact proof term for the current goal is Heq.
Assume Hxalt: order_rel X x a0.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hxnotxa Hxalt).
We prove the intermediate claim Hxc1: order_rel X x c1.
An exact proof term for the current goal is (Hcup1_lt x HxA1).
We prove the intermediate claim Hxd: order_rel X x d.
An exact proof term for the current goal is (order_rel_trans X x c1 d Hso HxX Hc1X HdX Hxc1 Hc1d).
We prove the intermediate claim HxI0: x ∈ {x0 ∈ X|order_rel X a0 x0 ∧ order_rel X x0 d}.
Apply (SepI X (λx0 : set ⇒ order_rel X a0 x0 ∧ order_rel X x0 d) x HxX) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Hxa0.
An exact proof term for the current goal is Hxd.
We prove the intermediate claim Hxb0: x ∈ b0.
rewrite the current goal using Hb0eq (from left to right).
An exact proof term for the current goal is HxI0.
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (Hb0subU x Hxb0).
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (andEL (x ∈ V) (order_rel X x u0) (SepE2 X (λx0 : set ⇒ x0 ∈ V ∧ order_rel X x0 u0) x HxA1)).
We prove the intermediate claim HxUV: x ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V x HxU HxV).
We prove the intermediate claim HxE: x ∈ Empty.
rewrite the current goal using HUVdisj (from right to left).
An exact proof term for the current goal is HxUV.
An exact proof term for the current goal is (EmptyE x HxE).
Assume Hb0L: (∃d ∈ X, b0 = {x ∈ X|order_rel X x d}).
Apply Hb0L to the current goal.
Let d be given.
Assume HdCore.
Apply HdCore to the current goal.
Assume HdX Hb0eq.
We prove the intermediate claim Hc1InL: c1 ∈ {x ∈ X|order_rel X x d}.
rewrite the current goal using Hb0eq (from right to left).
An exact proof term for the current goal is Hc1b0.
We prove the intermediate claim Hc1d: order_rel X c1 d.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X x0 d) c1 Hc1InL).
Set x to be the term v0.
We prove the intermediate claim HxA1w: x ∈ A1.
An exact proof term for the current goal is Hv0A1.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ x0 ∈ V ∧ order_rel X x0 u0) x HxA1w).
We prove the intermediate claim Hxc1: order_rel X x c1.
An exact proof term for the current goal is (Hcup1_lt x HxA1w).
We prove the intermediate claim Hxd: order_rel X x d.
An exact proof term for the current goal is (order_rel_trans X x c1 d Hso HxX Hc1X HdX Hxc1 Hc1d).
We prove the intermediate claim HxL: x ∈ {x0 ∈ X|order_rel X x0 d}.
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ order_rel X x0 d) x HxX Hxd).
We prove the intermediate claim Hxb0: x ∈ b0.
rewrite the current goal using Hb0eq (from left to right).
An exact proof term for the current goal is HxL.
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (Hb0subU x Hxb0).
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is Hv0V.
We prove the intermediate claim HxUV: x ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V x HxU HxV).
We prove the intermediate claim HxE: x ∈ Empty.
rewrite the current goal using HUVdisj (from right to left).
An exact proof term for the current goal is HxUV.
An exact proof term for the current goal is (EmptyE x HxE).
Assume Hb0R: (∃a0 ∈ X, b0 = {x ∈ X|order_rel X a0 x}).
Apply Hb0R to the current goal.
Let a0 be given.
Assume HaCore.
Apply HaCore to the current goal.
Assume Ha0X Hb0eq.
We prove the intermediate claim Hc1InR: c1 ∈ {x ∈ X|order_rel X a0 x}.
rewrite the current goal using Hb0eq (from right to left).
An exact proof term for the current goal is Hc1b0.
We prove the intermediate claim Ha0c1: order_rel X a0 c1.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X a0 x0) c1 Hc1InR).
We prove the intermediate claim HcontraUB: ¬ (∀x : set, x ∈ A1 → order_rel X x a0 ∨ x = a0).
Assume Hub: ∀x : set, x ∈ A1 → order_rel X x a0 ∨ x = a0.
We prove the intermediate claim Hc1a0: order_rel X c1 a0 ∨ c1 = a0.
An exact proof term for the current goal is (Hcleast1 a0 Ha0X Hub).
Apply Hc1a0 to the current goal.
Assume Hc1a0Rel: order_rel X c1 a0.
We prove the intermediate claim Ha0a0: order_rel X a0 a0.
An exact proof term for the current goal is (order_rel_trans X a0 c1 a0 Hso Ha0X Hc1X Ha0X Ha0c1 Hc1a0Rel).
An exact proof term for the current goal is ((order_rel_irref X a0) Ha0a0).
Assume Hc1eq: c1 = a0.
We prove the intermediate claim Ha0a0: order_rel X a0 a0.
rewrite the current goal using Hc1eq (from right to left) at position 2.
An exact proof term for the current goal is Ha0c1.
An exact proof term for the current goal is ((order_rel_irref X a0) Ha0a0).
We prove the intermediate claim Hexna: ∃x : set, ¬ (x ∈ A1 → order_rel X x a0 ∨ x = a0).
An exact proof term for the current goal is (not_all_ex_demorgan_i (λx : set ⇒ x ∈ A1 → order_rel X x a0 ∨ x = a0) HcontraUB).
Apply Hexna to the current goal.
Let x be given.
Assume HnotImp: ¬ (x ∈ A1 → order_rel X x a0 ∨ x = a0).
We prove the intermediate claim HxA1_and: x ∈ A1 ∧ ¬ (order_rel X x a0 ∨ x = a0).
An exact proof term for the current goal is (not_imp (x ∈ A1) (order_rel X x a0 ∨ x = a0) HnotImp).
We prove the intermediate claim HxA1: x ∈ A1.
An exact proof term for the current goal is (andEL (x ∈ A1) (¬ (order_rel X x a0 ∨ x = a0)) HxA1_and).
We prove the intermediate claim Hxnotle: ¬ (order_rel X x a0 ∨ x = a0).
An exact proof term for the current goal is (andER (x ∈ A1) (¬ (order_rel X x a0 ∨ x = a0)) HxA1_and).
We prove the intermediate claim Hxnot: ¬ (order_rel X x a0) ∧ x ≠ a0.
An exact proof term for the current goal is (not_or_and_demorgan (order_rel X x a0) (x = a0) Hxnotle).
We prove the intermediate claim Hxnotxa: ¬ (order_rel X x a0).
An exact proof term for the current goal is (andEL (¬ (order_rel X x a0)) (¬ (x = a0)) Hxnot).
We prove the intermediate claim Hxneq: x ≠ a0.
An exact proof term for the current goal is (andER (¬ (order_rel X x a0)) (¬ (x = a0)) Hxnot).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ x0 ∈ V ∧ order_rel X x0 u0) x HxA1).
We prove the intermediate claim Hxa0: order_rel X a0 x.
Apply (order_rel_trichotomy_or_impred X a0 x Hso Ha0X HxX (order_rel X a0 x)) to the current goal.
Assume Ha0x: order_rel X a0 x.
An exact proof term for the current goal is Ha0x.
Assume Heq: a0 = x.
Apply FalseE to the current goal.
Apply Hxneq to the current goal.
Use symmetry.
An exact proof term for the current goal is Heq.
Assume Hxalt: order_rel X x a0.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hxnotxa Hxalt).
We prove the intermediate claim Hxb0: x ∈ b0.
rewrite the current goal using Hb0eq (from left to right).
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ order_rel X a0 x0) x HxX Hxa0).
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (Hb0subU x Hxb0).
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (andEL (x ∈ V) (order_rel X x u0) (SepE2 X (λx0 : set ⇒ x0 ∈ V ∧ order_rel X x0 u0) x HxA1)).
We prove the intermediate claim HxUV: x ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V x HxU HxV).
We prove the intermediate claim HxE: x ∈ Empty.
rewrite the current goal using HUVdisj (from right to left).
An exact proof term for the current goal is HxUV.
An exact proof term for the current goal is (EmptyE x HxE).
Assume Hb0X: b0 = X.
We prove the intermediate claim Hv0U2: v0 ∈ U.
Apply Hb0subU to the current goal.
rewrite the current goal using Hb0X (from left to right).
An exact proof term for the current goal is Hv0X.
We prove the intermediate claim Hv0UV: v0 ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V v0 Hv0U2 Hv0V).
We prove the intermediate claim Hv0E: v0 ∈ Empty.
rewrite the current goal using HUVdisj (from right to left).
An exact proof term for the current goal is Hv0UV.
An exact proof term for the current goal is (EmptyE v0 Hv0E).
Assume Hc1V: c1 ∈ V.
We prove the intermediate claim Hu0UpperV: ∀a0 : set, a0 ∈ A1 → order_rel X a0 u0 ∨ a0 = u0.
Let a0 be given.
Assume Ha0A1: a0 ∈ A1.
We prove the intermediate claim Ha0Conj: a0 ∈ V ∧ order_rel X a0 u0.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ x0 ∈ V ∧ order_rel X x0 u0) a0 Ha0A1).
We prove the intermediate claim Hau0: order_rel X a0 u0.
An exact proof term for the current goal is (andER (a0 ∈ V) (order_rel X a0 u0) Ha0Conj).
Apply orIL to the current goal.
An exact proof term for the current goal is Hau0.
We prove the intermediate claim Hc1LeU0V: order_rel X c1 u0 ∨ c1 = u0.
An exact proof term for the current goal is (Hcleast1 u0 Hu0X Hu0UpperV).
We prove the intermediate claim Hc1LtU0: order_rel X c1 u0.
Apply Hc1LeU0V to the current goal.
Assume Hc1u0: order_rel X c1 u0.
An exact proof term for the current goal is Hc1u0.
Assume Hceq: c1 = u0.
Apply FalseE to the current goal.
We prove the intermediate claim Hu0V2: u0 ∈ V.
rewrite the current goal using Hceq (from right to left).
An exact proof term for the current goal is Hc1V.
We prove the intermediate claim Hu0UV: u0 ∈ U ∩ V.
An exact proof term for the current goal is (binintersectI U V u0 Hu0U Hu0V2).
We prove the intermediate claim Hu0E: u0 ∈ Empty.
rewrite the current goal using HUVdisj (from right to left).
An exact proof term for the current goal is Hu0UV.
An exact proof term for the current goal is (EmptyE u0 Hu0E).
Set Iu0 to be the term open_ray_lower X u0.
We prove the intermediate claim HIu0B: Iu0 ∈ order_topology_basis X.
An exact proof term for the current goal is (open_ray_lower_in_order_topology_basis X u0 Hu0X).
We prove the intermediate claim Hc1Iu0: c1 ∈ Iu0.
We prove the intermediate claim HIdef: Iu0 = {x ∈ X|order_rel X x u0}.
Use reflexivity.
rewrite the current goal using HIdef (from left to right).
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ order_rel X x0 u0) c1 Hc1X Hc1LtU0).
We prove the intermediate claim HexbV: ∃b0 ∈ order_topology_basis X, c1 ∈ b0 ∧ b0 ⊆ V.
An exact proof term for the current goal is (order_topology_local_basis_elem X V c1 Hso HVopen Hc1V).
Apply HexbV to the current goal.
Let b0 be given.
Assume Hb0Core.
Apply Hb0Core to the current goal.
Assume Hb0B Hb0Data.
Apply Hb0Data to the current goal.
Assume Hc1b0 Hb0subV.
We prove the intermediate claim HBasisOn: basis_on X (order_topology_basis X).
An exact proof term for the current goal is (order_topology_basis_is_basis X Hso).
We prove the intermediate claim Hexb3: ∃b3 ∈ order_topology_basis X, c1 ∈ b3 ∧ b3 ⊆ b0 ∩ Iu0.
An exact proof term for the current goal is (basis_on_refine X (order_topology_basis X) HBasisOn b0 Hb0B Iu0 HIu0B c1 Hc1b0 Hc1Iu0).
Apply Hexb3 to the current goal.
Let b3 be given.
Assume Hb3Core.
Apply Hb3Core to the current goal.
Assume Hb3B Hb3Data.
Apply Hb3Data to the current goal.
Assume Hc1b3 Hb3Sub.
We prove the intermediate claim Hcases: (∃a0 ∈ X, ∃d ∈ X, b3 = {x ∈ X|order_rel X a0 x ∧ order_rel X x d}) ∨ (∃d ∈ X, b3 = {x ∈ X|order_rel X x d}) ∨ (∃a0 ∈ X, b3 = {x ∈ X|order_rel X a0 x}) ∨ b3 = X.
An exact proof term for the current goal is (order_topology_basis_cases X b3 Hb3B).
Apply Hcases to the current goal.
Assume H123: (((∃a0 ∈ X, ∃d ∈ X, b3 = {x ∈ X|order_rel X a0 x ∧ order_rel X x d}) ∨ (∃d ∈ X, b3 = {x ∈ X|order_rel X x d})) ∨ (∃a0 ∈ X, b3 = {x ∈ X|order_rel X a0 x})).
Apply H123 to the current goal.
Assume H12: ((∃a0 ∈ X, ∃d ∈ X, b3 = {x ∈ X|order_rel X a0 x ∧ order_rel X x d}) ∨ (∃d ∈ X, b3 = {x ∈ X|order_rel X x d})).
Apply H12 to the current goal.
Assume Hb3I: (∃a0 ∈ X, ∃d ∈ X, b3 = {x ∈ X|order_rel X a0 x ∧ order_rel X x d}).
Apply Hb3I to the current goal.
Let a0 be given.
Assume HaCore.
Apply HaCore to the current goal.
Assume Ha0X HdEx.
Apply HdEx to the current goal.
Let d be given.
Assume HdCore.
Apply HdCore to the current goal.
Assume HdX Hb3eq.
We prove the intermediate claim Hc1InI0: c1 ∈ {x ∈ X|order_rel X a0 x ∧ order_rel X x d}.
rewrite the current goal using Hb3eq (from right to left).
An exact proof term for the current goal is Hc1b3.
We prove the intermediate claim Hc1Props: order_rel X a0 c1 ∧ order_rel X c1 d.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X a0 x0 ∧ order_rel X x0 d) c1 Hc1InI0).
We prove the intermediate claim Ha0c1: order_rel X a0 c1.
An exact proof term for the current goal is (andEL (order_rel X a0 c1) (order_rel X c1 d) Hc1Props).
We prove the intermediate claim Hc1d: order_rel X c1 d.
An exact proof term for the current goal is (andER (order_rel X a0 c1) (order_rel X c1 d) Hc1Props).
We prove the intermediate claim Hexz: ∃z : set, z ∈ X ∧ order_rel X c1 z ∧ order_rel X z d.
An exact proof term for the current goal is (Hbetween c1 d Hc1X HdX Hc1d).
Apply Hexz to the current goal.
Let z be given.
Assume HzConj.
We prove the intermediate claim HzCore: z ∈ X ∧ order_rel X c1 z.
An exact proof term for the current goal is (andEL (z ∈ X ∧ order_rel X c1 z) (order_rel X z d) HzConj).
We prove the intermediate claim HzX: z ∈ X.
An exact proof term for the current goal is (andEL (z ∈ X) (order_rel X c1 z) HzCore).
We prove the intermediate claim Hc1z: order_rel X c1 z.
An exact proof term for the current goal is (andER (z ∈ X) (order_rel X c1 z) HzCore).
We prove the intermediate claim HzI0: z ∈ {x ∈ X|order_rel X a0 x ∧ order_rel X x d}.
Apply (SepI X (λx0 : set ⇒ order_rel X a0 x0 ∧ order_rel X x0 d) z HzX) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is (order_rel_trans X a0 c1 z Hso Ha0X Hc1X HzX Ha0c1 Hc1z).
An exact proof term for the current goal is (andER (z ∈ X ∧ order_rel X c1 z) (order_rel X z d) HzConj).
We prove the intermediate claim Hzb3: z ∈ b3.
rewrite the current goal using Hb3eq (from left to right).
An exact proof term for the current goal is HzI0.
We prove the intermediate claim HzInInter: z ∈ b0 ∩ Iu0.
An exact proof term for the current goal is (Hb3Sub z Hzb3).
We prove the intermediate claim Hzb0: z ∈ b0.
An exact proof term for the current goal is (binintersectE1 b0 Iu0 z HzInInter).
We prove the intermediate claim HzIu0: z ∈ Iu0.
An exact proof term for the current goal is (binintersectE2 b0 Iu0 z HzInInter).
We prove the intermediate claim HzV: z ∈ V.
An exact proof term for the current goal is (Hb0subV z Hzb0).
We prove the intermediate claim Hzltu0: order_rel X z u0.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X x0 u0) z HzIu0).
We prove the intermediate claim HzA1: z ∈ A1.
Apply (SepI X (λx0 : set ⇒ x0 ∈ V ∧ order_rel X x0 u0) z HzX) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HzV.
An exact proof term for the current goal is Hzltu0.
Apply (Hcup1 z HzA1) to the current goal.
Assume Hzltc1: order_rel X z c1.
We prove the intermediate claim Hcc: order_rel X c1 c1.
An exact proof term for the current goal is (order_rel_trans X c1 z c1 Hso Hc1X HzX Hc1X Hc1z Hzltc1).
An exact proof term for the current goal is ((order_rel_irref X c1) Hcc).
Assume Hzeq: z = c1.
We prove the intermediate claim Hcc: order_rel X c1 c1.
rewrite the current goal using Hzeq (from right to left) at position 2.
An exact proof term for the current goal is Hc1z.
An exact proof term for the current goal is ((order_rel_irref X c1) Hcc).
Assume Hb3L: (∃d ∈ X, b3 = {x ∈ X|order_rel X x d}).
Apply Hb3L to the current goal.
Let d be given.
Assume HdCore.
Apply HdCore to the current goal.
Assume HdX Hb3eq.
We prove the intermediate claim Hc1InL: c1 ∈ {x ∈ X|order_rel X x d}.
rewrite the current goal using Hb3eq (from right to left).
An exact proof term for the current goal is Hc1b3.
We prove the intermediate claim Hc1d: order_rel X c1 d.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X x0 d) c1 Hc1InL).
We prove the intermediate claim Hexz: ∃z : set, z ∈ X ∧ order_rel X c1 z ∧ order_rel X z d.
An exact proof term for the current goal is (Hbetween c1 d Hc1X HdX Hc1d).
Apply Hexz to the current goal.
Let z be given.
Assume HzConj.
We prove the intermediate claim HzCore: z ∈ X ∧ order_rel X c1 z.
An exact proof term for the current goal is (andEL (z ∈ X ∧ order_rel X c1 z) (order_rel X z d) HzConj).
We prove the intermediate claim HzX: z ∈ X.
An exact proof term for the current goal is (andEL (z ∈ X) (order_rel X c1 z) HzCore).
We prove the intermediate claim Hc1z: order_rel X c1 z.
An exact proof term for the current goal is (andER (z ∈ X) (order_rel X c1 z) HzCore).
We prove the intermediate claim Hzld: order_rel X z d.
An exact proof term for the current goal is (andER (z ∈ X ∧ order_rel X c1 z) (order_rel X z d) HzConj).
We prove the intermediate claim HzL: z ∈ {x ∈ X|order_rel X x d}.
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ order_rel X x0 d) z HzX Hzld).
We prove the intermediate claim Hzb3: z ∈ b3.
rewrite the current goal using Hb3eq (from left to right).
An exact proof term for the current goal is HzL.
We prove the intermediate claim HzInInter: z ∈ b0 ∩ Iu0.
An exact proof term for the current goal is (Hb3Sub z Hzb3).
We prove the intermediate claim Hzb0: z ∈ b0.
An exact proof term for the current goal is (binintersectE1 b0 Iu0 z HzInInter).
We prove the intermediate claim HzIu0: z ∈ Iu0.
An exact proof term for the current goal is (binintersectE2 b0 Iu0 z HzInInter).
We prove the intermediate claim HzV: z ∈ V.
An exact proof term for the current goal is (Hb0subV z Hzb0).
We prove the intermediate claim Hzltu0: order_rel X z u0.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X x0 u0) z HzIu0).
We prove the intermediate claim HzA1: z ∈ A1.
Apply (SepI X (λx0 : set ⇒ x0 ∈ V ∧ order_rel X x0 u0) z HzX) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HzV.
An exact proof term for the current goal is Hzltu0.
Apply (Hcup1 z HzA1) to the current goal.
Assume Hzltc1: order_rel X z c1.
We prove the intermediate claim Hcc: order_rel X c1 c1.
An exact proof term for the current goal is (order_rel_trans X c1 z c1 Hso Hc1X HzX Hc1X Hc1z Hzltc1).
An exact proof term for the current goal is ((order_rel_irref X c1) Hcc).
Assume Hzeq: z = c1.
We prove the intermediate claim Hcc: order_rel X c1 c1.
rewrite the current goal using Hzeq (from right to left) at position 2.
An exact proof term for the current goal is Hc1z.
An exact proof term for the current goal is ((order_rel_irref X c1) Hcc).
Assume Hb3R: (∃a0 ∈ X, b3 = {x ∈ X|order_rel X a0 x}).
Apply Hb3R to the current goal.
Let a0 be given.
Assume HaCore.
Apply HaCore to the current goal.
Assume Ha0X Hb3eq.
We prove the intermediate claim Hc1InR: c1 ∈ {x ∈ X|order_rel X a0 x}.
rewrite the current goal using Hb3eq (from right to left).
An exact proof term for the current goal is Hc1b3.
We prove the intermediate claim Ha0c1: order_rel X a0 c1.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X a0 x0) c1 Hc1InR).
We prove the intermediate claim Ha0u0: order_rel X a0 u0.
An exact proof term for the current goal is (order_rel_trans X a0 c1 u0 Hso Ha0X Hc1X Hu0X Ha0c1 Hc1LtU0).
We prove the intermediate claim Hu0b3: u0 ∈ b3.
rewrite the current goal using Hb3eq (from left to right).
An exact proof term for the current goal is (SepI X (λx0 : set ⇒ order_rel X a0 x0) u0 Hu0X Ha0u0).
We prove the intermediate claim Hu0InInter: u0 ∈ b0 ∩ Iu0.
An exact proof term for the current goal is (Hb3Sub u0 Hu0b3).
We prove the intermediate claim Hu0Iu0: u0 ∈ Iu0.
An exact proof term for the current goal is (binintersectE2 b0 Iu0 u0 Hu0InInter).
We prove the intermediate claim Hu0ltu0: order_rel X u0 u0.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X x0 u0) u0 Hu0Iu0).
An exact proof term for the current goal is ((order_rel_irref X u0) Hu0ltu0).
Assume Hb3X: b3 = X.
We prove the intermediate claim Hu0b3: u0 ∈ b3.
rewrite the current goal using Hb3X (from left to right).
An exact proof term for the current goal is Hu0X.
We prove the intermediate claim Hu0InInter: u0 ∈ b0 ∩ Iu0.
An exact proof term for the current goal is (Hb3Sub u0 Hu0b3).
We prove the intermediate claim Hu0Iu0: u0 ∈ Iu0.
An exact proof term for the current goal is (binintersectE2 b0 Iu0 u0 Hu0InInter).
We prove the intermediate claim Hu0ltu0: order_rel X u0 u0.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X x0 u0) u0 Hu0Iu0).
An exact proof term for the current goal is ((order_rel_irref X u0) Hu0ltu0).
∎