Let X be given.
Assume Hso: simply_ordered_set X.
We will prove basis_on X (order_topology_basis X).
Set A to be the term order_topology_basis X ⊆ đ’Ģ X.
Set Bcov to be the term (∀x ∈ X, ∃b ∈ (order_topology_basis X), x ∈ b).
Set Bref to be the term (∀b1 ∈ (order_topology_basis X), ∀b2 ∈ (order_topology_basis X), ∀x : set, x ∈ b1 → x ∈ b2 → ∃b3 ∈ (order_topology_basis X), x ∈ b3 ∧ b3 ⊆ b1 ∩ b2).
We prove the intermediate claim Hab: A ∧ Bcov.
Apply andI to the current goal.
We will prove order_topology_basis X ⊆ đ’Ģ X.
Let I be given.
Assume HI: I ∈ order_topology_basis X.
We will prove I ∈ đ’Ģ X.
Set Bold to be the term ({I0 ∈ đ’Ģ X|∃a ∈ X, ∃b ∈ X, I0 = {x ∈ X|order_rel X a x ∧ order_rel X x b}} âˆĒ {I0 ∈ đ’Ģ X|∃b ∈ X, I0 = {x ∈ X|order_rel X x b}} âˆĒ {I0 ∈ đ’Ģ X|∃a ∈ X, I0 = {x ∈ X|order_rel X a x}}).
Apply (binunionE Bold {X} I HI) to the current goal.
Assume HI0: I ∈ Bold.
Apply (binunionE ({I0 ∈ đ’Ģ X|∃a ∈ X, ∃b ∈ X, I0 = {x ∈ X|order_rel X a x ∧ order_rel X x b}} âˆĒ {I0 ∈ đ’Ģ X|∃b ∈ X, I0 = {x ∈ X|order_rel X x b}}) ({I0 ∈ đ’Ģ X|∃a ∈ X, I0 = {x ∈ X|order_rel X a x}}) I HI0) to the current goal.
Assume HI12: I ∈ ({I0 ∈ đ’Ģ X|∃a ∈ X, ∃b ∈ X, I0 = {x ∈ X|order_rel X a x ∧ order_rel X x b}} âˆĒ {I0 ∈ đ’Ģ X|∃b ∈ X, I0 = {x ∈ X|order_rel X x b}}).
Apply (binunionE ({I0 ∈ đ’Ģ X|∃a ∈ X, ∃b ∈ X, I0 = {x ∈ X|order_rel X a x ∧ order_rel X x b}}) ({I0 ∈ đ’Ģ X|∃b ∈ X, I0 = {x ∈ X|order_rel X x b}}) I HI12) to the current goal.
Assume HI1: I ∈ {I0 ∈ đ’Ģ X|∃a ∈ X, ∃b ∈ X, I0 = {x ∈ X|order_rel X a x ∧ order_rel X x b}}.
An exact proof term for the current goal is (SepE1 (đ’Ģ X) (ÎģI0 : set ⇒ ∃a ∈ X, ∃b ∈ X, I0 = {x ∈ X|order_rel X a x ∧ order_rel X x b}) I HI1).
Assume HI2: I ∈ {I0 ∈ đ’Ģ X|∃b ∈ X, I0 = {x ∈ X|order_rel X x b}}.
An exact proof term for the current goal is (SepE1 (đ’Ģ X) (ÎģI0 : set ⇒ ∃b ∈ X, I0 = {x ∈ X|order_rel X x b}) I HI2).
Assume HI3: I ∈ {I0 ∈ đ’Ģ X|∃a ∈ X, I0 = {x ∈ X|order_rel X a x}}.
An exact proof term for the current goal is (SepE1 (đ’Ģ X) (ÎģI0 : set ⇒ ∃a ∈ X, I0 = {x ∈ X|order_rel X a x}) I HI3).
Assume HIX: I ∈ {X}.
We prove the intermediate claim HIEq: I = X.
An exact proof term for the current goal is (SingE X I HIX).
rewrite the current goal using HIEq (from left to right).
An exact proof term for the current goal is (Self_In_Power X).
We will prove ∀x ∈ X, ∃b ∈ (order_topology_basis X), x ∈ b.
Let x be given.
Assume HxX: x ∈ X.
We use X to witness the existential quantifier.
Apply andI to the current goal.
Set Bold to be the term ({I0 ∈ đ’Ģ X|∃a ∈ X, ∃b ∈ X, I0 = {x0 ∈ X|order_rel X a x0 ∧ order_rel X x0 b}} âˆĒ {I0 ∈ đ’Ģ X|∃b ∈ X, I0 = {x0 ∈ X|order_rel X x0 b}} âˆĒ {I0 ∈ đ’Ģ X|∃a ∈ X, I0 = {x0 ∈ X|order_rel X a x0}}).
An exact proof term for the current goal is (binunionI2 Bold {X} X (SingI X)).
An exact proof term for the current goal is HxX.
We prove the intermediate claim Href: Bref.
Let b1 be given.
Assume Hb1: b1 ∈ order_topology_basis X.
Let b2 be given.
Assume Hb2: b2 ∈ order_topology_basis X.
Let x be given.
Assume Hx1: x ∈ b1.
Assume Hx2: x ∈ b2.
We will prove ∃b3 ∈ (order_topology_basis X), x ∈ b3 ∧ b3 ⊆ b1 ∩ b2.
Set Bold to be the term ({I0 ∈ đ’Ģ X|∃a ∈ X, ∃b ∈ X, I0 = {x0 ∈ X|order_rel X a x0 ∧ order_rel X x0 b}} âˆĒ {I0 ∈ đ’Ģ X|∃b ∈ X, I0 = {x0 ∈ X|order_rel X x0 b}} âˆĒ {I0 ∈ đ’Ģ X|∃a ∈ X, I0 = {x0 ∈ X|order_rel X a x0}}).
We prove the intermediate claim HsubPow: order_topology_basis X ⊆ đ’Ģ X.
An exact proof term for the current goal is (andEL A Bcov Hab).
Apply (binunionE Bold {X} b1 Hb1) to the current goal.
Assume Hb1old: b1 ∈ Bold.
Apply (binunionE Bold {X} b2 Hb2) to the current goal.
Assume Hb2old: b2 ∈ Bold.
Set Aint to be the term {I0 ∈ đ’Ģ X|∃a ∈ X, ∃b ∈ X, I0 = {x0 ∈ X|order_rel X a x0 ∧ order_rel X x0 b}}.
Set Blow to be the term {I0 ∈ đ’Ģ X|∃b ∈ X, I0 = {x0 ∈ X|order_rel X x0 b}}.
Set Cup to be the term {I0 ∈ đ’Ģ X|∃a ∈ X, I0 = {x0 ∈ X|order_rel X a x0}}.
We prove the intermediate claim HBdef: Bold = (Aint âˆĒ Blow âˆĒ Cup).
Use reflexivity.
We prove the intermediate claim Hb1tri: b1 ∈ (Aint âˆĒ Blow âˆĒ Cup).
rewrite the current goal using HBdef (from right to left).
An exact proof term for the current goal is Hb1old.
We prove the intermediate claim Hb2tri: b2 ∈ (Aint âˆĒ Blow âˆĒ Cup).
rewrite the current goal using HBdef (from right to left).
An exact proof term for the current goal is Hb2old.
Apply (binunionE (Aint âˆĒ Blow) Cup b1 Hb1tri) to the current goal.
Assume Hb1AB: b1 ∈ (Aint âˆĒ Blow).
Apply (binunionE Aint Blow b1 Hb1AB) to the current goal.
Assume Hb1A: b1 ∈ Aint.
We prove the intermediate claim Hexab1: ∃a1 ∈ X, ∃b1x ∈ X, b1 = {x0 ∈ X|order_rel X a1 x0 ∧ order_rel X x0 b1x}.
An exact proof term for the current goal is (SepE2 (đ’Ģ X) (ÎģI0 : set ⇒ ∃a1 ∈ X, ∃b1x ∈ X, I0 = {x0 ∈ X|order_rel X a1 x0 ∧ order_rel X x0 b1x}) b1 Hb1A).
Apply Hexab1 to the current goal.
Let a1 be given.
Assume Ha1core: a1 ∈ X ∧ ∃b1x ∈ X, b1 = {x0 ∈ X|order_rel X a1 x0 ∧ order_rel X x0 b1x}.
Apply Ha1core to the current goal.
Assume Ha1X: a1 ∈ X.
Assume Hexb1x: ∃b1x ∈ X, b1 = {x0 ∈ X|order_rel X a1 x0 ∧ order_rel X x0 b1x}.
Apply Hexb1x to the current goal.
Let b1x be given.
Assume Hb1xcore: b1x ∈ X ∧ b1 = {x0 ∈ X|order_rel X a1 x0 ∧ order_rel X x0 b1x}.
Apply Hb1xcore to the current goal.
Assume Hb1xX: b1x ∈ X.
Assume Hb1eq: b1 = {x0 ∈ X|order_rel X a1 x0 ∧ order_rel X x0 b1x}.
Apply (binunionE (Aint âˆĒ Blow) Cup b2 Hb2tri) to the current goal.
Assume Hb2AB: b2 ∈ (Aint âˆĒ Blow).
Apply (binunionE Aint Blow b2 Hb2AB) to the current goal.
Assume Hb2A: b2 ∈ Aint.
We prove the intermediate claim Hexab2: ∃a2 ∈ X, ∃b2x ∈ X, b2 = {x0 ∈ X|order_rel X a2 x0 ∧ order_rel X x0 b2x}.
An exact proof term for the current goal is (SepE2 (đ’Ģ X) (ÎģI0 : set ⇒ ∃a2 ∈ X, ∃b2x ∈ X, I0 = {x0 ∈ X|order_rel X a2 x0 ∧ order_rel X x0 b2x}) b2 Hb2A).
Apply Hexab2 to the current goal.
Let a2 be given.
Assume Ha2core: a2 ∈ X ∧ ∃b2x ∈ X, b2 = {x0 ∈ X|order_rel X a2 x0 ∧ order_rel X x0 b2x}.
Apply Ha2core to the current goal.
Assume Ha2X: a2 ∈ X.
Assume Hexb2x: ∃b2x ∈ X, b2 = {x0 ∈ X|order_rel X a2 x0 ∧ order_rel X x0 b2x}.
Apply Hexb2x to the current goal.
Let b2x be given.
Assume Hb2xcore: b2x ∈ X ∧ b2 = {x0 ∈ X|order_rel X a2 x0 ∧ order_rel X x0 b2x}.
Apply Hb2xcore to the current goal.
Assume Hb2xX: b2x ∈ X.
Assume Hb2eq: b2 = {x0 ∈ X|order_rel X a2 x0 ∧ order_rel X x0 b2x}.
An exact proof term for the current goal is (order_topology_interval_refine X a1 b1x a2 b2x b1 b2 x Hso Ha1X Hb1xX Ha2X Hb2xX Hb1eq Hb2eq Hx1 Hx2).
Assume Hb2B: b2 ∈ Blow.
We prove the intermediate claim Hexb0: ∃b0 ∈ X, b2 = {x0 ∈ X|order_rel X x0 b0}.
An exact proof term for the current goal is (SepE2 (đ’Ģ X) (ÎģI0 : set ⇒ ∃b0 ∈ X, I0 = {x0 ∈ X|order_rel X x0 b0}) b2 Hb2B).
Apply Hexb0 to the current goal.
Let b0 be given.
Assume Hb0core: b0 ∈ X ∧ b2 = {x0 ∈ X|order_rel X x0 b0}.
Apply Hb0core to the current goal.
Assume Hb0X: b0 ∈ X.
Assume Hb2eq: b2 = {x0 ∈ X|order_rel X x0 b0}.
Apply (order_rel_trichotomy_or_impred X b1x b0 Hso Hb1xX Hb0X (∃b3 ∈ (order_topology_basis X), x ∈ b3 ∧ b3 ⊆ b1 ∩ b2)) to the current goal.
Assume Hb1xlt: order_rel X b1x b0.
We use b1 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (binunionI1 Bold {X} b1 Hb1old).
Apply andI to the current goal.
An exact proof term for the current goal is Hx1.
We will prove b1 ⊆ b1 ∩ b2.
Let y be given.
Assume Hy: y ∈ b1.
We will prove y ∈ b1 ∊ b2.
We prove the intermediate claim Hyin: y ∈ {x0 ∈ X|order_rel X a1 x0 ∧ order_rel X x0 b1x}.
rewrite the current goal using Hb1eq (from right to left).
An exact proof term for the current goal is Hy.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (SepE1 X (Îģx0 : set ⇒ order_rel X a1 x0 ∧ order_rel X x0 b1x) y Hyin).
We prove the intermediate claim Hyrel: order_rel X a1 y ∧ order_rel X y b1x.
An exact proof term for the current goal is (SepE2 X (Îģx0 : set ⇒ order_rel X a1 x0 ∧ order_rel X x0 b1x) y Hyin).
We prove the intermediate claim Hyub1: order_rel X y b1x.
An exact proof term for the current goal is (andER (order_rel X a1 y) (order_rel X y b1x) Hyrel).
We prove the intermediate claim Hyub0: order_rel X y b0.
An exact proof term for the current goal is (order_rel_trans X y b1x b0 Hso HyX Hb1xX Hb0X Hyub1 Hb1xlt).
We prove the intermediate claim Hyb2: y ∈ b2.
rewrite the current goal using Hb2eq (from left to right).
An exact proof term for the current goal is (SepI X (Îģx0 : set ⇒ order_rel X x0 b0) y HyX Hyub0).
An exact proof term for the current goal is (binintersectI b1 b2 y Hy Hyb2).
Assume Hbeq: b1x = b0.
We use b1 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (binunionI1 Bold {X} b1 Hb1old).
Apply andI to the current goal.
An exact proof term for the current goal is Hx1.
We will prove b1 ⊆ b1 ∩ b2.
Let y be given.
Assume Hy: y ∈ b1.
We will prove y ∈ b1 ∊ b2.
We prove the intermediate claim Hyin: y ∈ {x0 ∈ X|order_rel X a1 x0 ∧ order_rel X x0 b1x}.
rewrite the current goal using Hb1eq (from right to left).
An exact proof term for the current goal is Hy.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (SepE1 X (Îģx0 : set ⇒ order_rel X a1 x0 ∧ order_rel X x0 b1x) y Hyin).
We prove the intermediate claim Hyrel: order_rel X a1 y ∧ order_rel X y b1x.
An exact proof term for the current goal is (SepE2 X (Îģx0 : set ⇒ order_rel X a1 x0 ∧ order_rel X x0 b1x) y Hyin).
We prove the intermediate claim Hyub1: order_rel X y b1x.
An exact proof term for the current goal is (andER (order_rel X a1 y) (order_rel X y b1x) Hyrel).
We prove the intermediate claim Hyub0: order_rel X y b0.
rewrite the current goal using Hbeq (from right to left).
An exact proof term for the current goal is Hyub1.
We prove the intermediate claim Hyb2: y ∈ b2.
rewrite the current goal using Hb2eq (from left to right).
An exact proof term for the current goal is (SepI X (Îģx0 : set ⇒ order_rel X x0 b0) y HyX Hyub0).
An exact proof term for the current goal is (binintersectI b1 b2 y Hy Hyb2).
Assume Hb0lt: order_rel X b0 b1x.
Set b3 to be the term {x0 ∈ X|order_rel X a1 x0 ∧ order_rel X x0 b0}.
We use b3 to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim Hb3Pow: b3 ∈ đ’Ģ X.
Apply PowerI to the current goal.
Let y be given.
Assume Hy: y ∈ b3.
An exact proof term for the current goal is (SepE1 X (Îģx0 : set ⇒ order_rel X a1 x0 ∧ order_rel X x0 b0) y Hy).
We prove the intermediate claim Hexa: ∃a ∈ X, ∃b ∈ X, b3 = {x0 ∈ X|order_rel X a x0 ∧ order_rel X x0 b}.
We use a1 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Ha1X.
We use b0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hb0X.
Use reflexivity.
We prove the intermediate claim Hb3A: b3 ∈ Aint.
An exact proof term for the current goal is (SepI (đ’Ģ X) (ÎģI0 : set ⇒ ∃a ∈ X, ∃b ∈ X, I0 = {x0 ∈ X|order_rel X a x0 ∧ order_rel X x0 b}) b3 Hb3Pow Hexa).
We prove the intermediate claim Hb3tri: b3 ∈ (Aint âˆĒ Blow âˆĒ Cup).
An exact proof term for the current goal is (binunionI1 (Aint âˆĒ Blow) Cup b3 (binunionI1 Aint Blow b3 Hb3A)).
We prove the intermediate claim Hb3Bold: b3 ∈ Bold.
rewrite the current goal using HBdef (from left to right).
An exact proof term for the current goal is Hb3tri.
An exact proof term for the current goal is (binunionI1 Bold {X} b3 Hb3Bold).
Apply andI to the current goal.
We prove the intermediate claim HxIn1: x ∈ {x0 ∈ X|order_rel X a1 x0 ∧ order_rel X x0 b1x}.
rewrite the current goal using Hb1eq (from right to left).
An exact proof term for the current goal is Hx1.
We prove the intermediate claim HxIn2: x ∈ {x0 ∈ X|order_rel X x0 b0}.
rewrite the current goal using Hb2eq (from right to left).
An exact proof term for the current goal is Hx2.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (Îģx0 : set ⇒ order_rel X x0 b0) x HxIn2).
We prove the intermediate claim Hxrel2: order_rel X x b0.
An exact proof term for the current goal is (SepE2 X (Îģx0 : set ⇒ order_rel X x0 b0) x HxIn2).
We prove the intermediate claim Hxrel1: order_rel X a1 x ∧ order_rel X x b1x.
An exact proof term for the current goal is (SepE2 X (Îģx0 : set ⇒ order_rel X a1 x0 ∧ order_rel X x0 b1x) x HxIn1).
We prove the intermediate claim Hxa1: order_rel X a1 x.
An exact proof term for the current goal is (andEL (order_rel X a1 x) (order_rel X x b1x) Hxrel1).
An exact proof term for the current goal is (SepI X (Îģx0 : set ⇒ order_rel X a1 x0 ∧ order_rel X x0 b0) x HxX (andI (order_rel X a1 x) (order_rel X x b0) Hxa1 Hxrel2)).
We will prove b3 ⊆ b1 ∩ b2.
Let y be given.
Assume Hy3: y ∈ b3.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (SepE1 X (Îģx0 : set ⇒ order_rel X a1 x0 ∧ order_rel X x0 b0) y Hy3).
We prove the intermediate claim Hyrel: order_rel X a1 y ∧ order_rel X y b0.
An exact proof term for the current goal is (SepE2 X (Îģx0 : set ⇒ order_rel X a1 x0 ∧ order_rel X x0 b0) y Hy3).
We prove the intermediate claim Hyla1: order_rel X a1 y.
An exact proof term for the current goal is (andEL (order_rel X a1 y) (order_rel X y b0) Hyrel).
We prove the intermediate claim Hyub0: order_rel X y b0.
An exact proof term for the current goal is (andER (order_rel X a1 y) (order_rel X y b0) Hyrel).
We prove the intermediate claim Hyub1x: order_rel X y b1x.
An exact proof term for the current goal is (order_rel_trans X y b0 b1x Hso HyX Hb0X Hb1xX Hyub0 Hb0lt).
We prove the intermediate claim Hyb1: y ∈ b1.
rewrite the current goal using Hb1eq (from left to right).
An exact proof term for the current goal is (SepI X (Îģx0 : set ⇒ order_rel X a1 x0 ∧ order_rel X x0 b1x) y HyX (andI (order_rel X a1 y) (order_rel X y b1x) Hyla1 Hyub1x)).
We prove the intermediate claim Hyb2: y ∈ b2.
rewrite the current goal using Hb2eq (from left to right).
An exact proof term for the current goal is (SepI X (Îģx0 : set ⇒ order_rel X x0 b0) y HyX Hyub0).
An exact proof term for the current goal is (binintersectI b1 b2 y Hyb1 Hyb2).
Assume Hb2C: b2 ∈ Cup.
We prove the intermediate claim Hexa0: ∃a0 ∈ X, b2 = {x0 ∈ X|order_rel X a0 x0}.
An exact proof term for the current goal is (SepE2 (đ’Ģ X) (ÎģI0 : set ⇒ ∃a0 ∈ X, I0 = {x0 ∈ X|order_rel X a0 x0}) b2 Hb2C).
Apply Hexa0 to the current goal.
Let a0 be given.
Assume Ha0core: a0 ∈ X ∧ b2 = {x0 ∈ X|order_rel X a0 x0}.
Apply Ha0core to the current goal.
Assume Ha0X: a0 ∈ X.
Assume Hb2eq: b2 = {x0 ∈ X|order_rel X a0 x0}.
Apply (order_rel_trichotomy_or_impred X a0 a1 Hso Ha0X Ha1X (∃b3 ∈ (order_topology_basis X), x ∈ b3 ∧ b3 ⊆ b1 ∩ b2)) to the current goal.
Assume Ha0lt: order_rel X a0 a1.
We use b1 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (binunionI1 Bold {X} b1 Hb1old).
Apply andI to the current goal.
An exact proof term for the current goal is Hx1.
We will prove b1 ⊆ b1 ∩ b2.
Let y be given.
Assume Hy: y ∈ b1.
We will prove y ∈ b1 ∊ b2.
We prove the intermediate claim Hyin: y ∈ {x0 ∈ X|order_rel X a1 x0 ∧ order_rel X x0 b1x}.
rewrite the current goal using Hb1eq (from right to left).
An exact proof term for the current goal is Hy.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (SepE1 X (Îģx0 : set ⇒ order_rel X a1 x0 ∧ order_rel X x0 b1x) y Hyin).
We prove the intermediate claim Hyrel: order_rel X a1 y ∧ order_rel X y b1x.
An exact proof term for the current goal is (SepE2 X (Îģx0 : set ⇒ order_rel X a1 x0 ∧ order_rel X x0 b1x) y Hyin).
We prove the intermediate claim Hyla1: order_rel X a1 y.
An exact proof term for the current goal is (andEL (order_rel X a1 y) (order_rel X y b1x) Hyrel).
We prove the intermediate claim Hyla0: order_rel X a0 y.
An exact proof term for the current goal is (order_rel_trans X a0 a1 y Hso Ha0X Ha1X HyX Ha0lt Hyla1).
We prove the intermediate claim Hyb2: y ∈ b2.
rewrite the current goal using Hb2eq (from left to right).
An exact proof term for the current goal is (SepI X (Îģx0 : set ⇒ order_rel X a0 x0) y HyX Hyla0).
An exact proof term for the current goal is (binintersectI b1 b2 y Hy Hyb2).
Assume Haeq: a0 = a1.
We use b1 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (binunionI1 Bold {X} b1 Hb1old).
Apply andI to the current goal.
An exact proof term for the current goal is Hx1.
We will prove b1 ⊆ b1 ∩ b2.
Let y be given.
Assume Hy: y ∈ b1.
We will prove y ∈ b1 ∊ b2.
We prove the intermediate claim Hyin: y ∈ {x0 ∈ X|order_rel X a1 x0 ∧ order_rel X x0 b1x}.
rewrite the current goal using Hb1eq (from right to left).
An exact proof term for the current goal is Hy.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (SepE1 X (Îģx0 : set ⇒ order_rel X a1 x0 ∧ order_rel X x0 b1x) y Hyin).
We prove the intermediate claim Hyrel: order_rel X a1 y ∧ order_rel X y b1x.
An exact proof term for the current goal is (SepE2 X (Îģx0 : set ⇒ order_rel X a1 x0 ∧ order_rel X x0 b1x) y Hyin).
We prove the intermediate claim Hyla1: order_rel X a1 y.
An exact proof term for the current goal is (andEL (order_rel X a1 y) (order_rel X y b1x) Hyrel).
We prove the intermediate claim Hyla0: order_rel X a0 y.
rewrite the current goal using Haeq (from left to right).
An exact proof term for the current goal is Hyla1.
We prove the intermediate claim Hyb2: y ∈ b2.
rewrite the current goal using Hb2eq (from left to right).
An exact proof term for the current goal is (SepI X (Îģx0 : set ⇒ order_rel X a0 x0) y HyX Hyla0).
An exact proof term for the current goal is (binintersectI b1 b2 y Hy Hyb2).
Assume Ha1lt: order_rel X a1 a0.
Set b3 to be the term {x0 ∈ X|order_rel X a0 x0 ∧ order_rel X x0 b1x}.
We use b3 to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim Hb3Pow: b3 ∈ đ’Ģ X.
Apply PowerI to the current goal.
Let y be given.
Assume Hy: y ∈ b3.
An exact proof term for the current goal is (SepE1 X (Îģx0 : set ⇒ order_rel X a0 x0 ∧ order_rel X x0 b1x) y Hy).
We prove the intermediate claim Hexa: ∃a ∈ X, ∃b ∈ X, b3 = {x0 ∈ X|order_rel X a x0 ∧ order_rel X x0 b}.
We use a0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Ha0X.
We use b1x to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hb1xX.
Use reflexivity.
We prove the intermediate claim Hb3A: b3 ∈ Aint.
An exact proof term for the current goal is (SepI (đ’Ģ X) (ÎģI0 : set ⇒ ∃a ∈ X, ∃b ∈ X, I0 = {x0 ∈ X|order_rel X a x0 ∧ order_rel X x0 b}) b3 Hb3Pow Hexa).
We prove the intermediate claim Hb3tri: b3 ∈ (Aint âˆĒ Blow âˆĒ Cup).
An exact proof term for the current goal is (binunionI1 (Aint âˆĒ Blow) Cup b3 (binunionI1 Aint Blow b3 Hb3A)).
We prove the intermediate claim Hb3Bold: b3 ∈ Bold.
rewrite the current goal using HBdef (from left to right).
An exact proof term for the current goal is Hb3tri.
An exact proof term for the current goal is (binunionI1 Bold {X} b3 Hb3Bold).
Apply andI to the current goal.
We prove the intermediate claim HxIn1: x ∈ {x0 ∈ X|order_rel X a1 x0 ∧ order_rel X x0 b1x}.
rewrite the current goal using Hb1eq (from right to left).
An exact proof term for the current goal is Hx1.
We prove the intermediate claim HxIn2: x ∈ {x0 ∈ X|order_rel X a0 x0}.
rewrite the current goal using Hb2eq (from right to left).
An exact proof term for the current goal is Hx2.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (Îģx0 : set ⇒ order_rel X a0 x0) x HxIn2).
We prove the intermediate claim Hxa0: order_rel X a0 x.
An exact proof term for the current goal is (SepE2 X (Îģx0 : set ⇒ order_rel X a0 x0) x HxIn2).
We prove the intermediate claim Hxrel1: order_rel X a1 x ∧ order_rel X x b1x.
An exact proof term for the current goal is (SepE2 X (Îģx0 : set ⇒ order_rel X a1 x0 ∧ order_rel X x0 b1x) x HxIn1).
We prove the intermediate claim Hxb1x: order_rel X x b1x.
An exact proof term for the current goal is (andER (order_rel X a1 x) (order_rel X x b1x) Hxrel1).
An exact proof term for the current goal is (SepI X (Îģx0 : set ⇒ order_rel X a0 x0 ∧ order_rel X x0 b1x) x HxX (andI (order_rel X a0 x) (order_rel X x b1x) Hxa0 Hxb1x)).
We will prove b3 ⊆ b1 ∩ b2.
Let y be given.
Assume Hy3: y ∈ b3.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (SepE1 X (Îģx0 : set ⇒ order_rel X a0 x0 ∧ order_rel X x0 b1x) y Hy3).
We prove the intermediate claim Hyrel: order_rel X a0 y ∧ order_rel X y b1x.
An exact proof term for the current goal is (SepE2 X (Îģx0 : set ⇒ order_rel X a0 x0 ∧ order_rel X x0 b1x) y Hy3).
We prove the intermediate claim Hyla0: order_rel X a0 y.
An exact proof term for the current goal is (andEL (order_rel X a0 y) (order_rel X y b1x) Hyrel).
We prove the intermediate claim Hyub1x: order_rel X y b1x.
An exact proof term for the current goal is (andER (order_rel X a0 y) (order_rel X y b1x) Hyrel).
We prove the intermediate claim Hyla1: order_rel X a1 y.
An exact proof term for the current goal is (order_rel_trans X a1 a0 y Hso Ha1X Ha0X HyX Ha1lt Hyla0).
We prove the intermediate claim Hyb1: y ∈ b1.
rewrite the current goal using Hb1eq (from left to right).
An exact proof term for the current goal is (SepI X (Îģx0 : set ⇒ order_rel X a1 x0 ∧ order_rel X x0 b1x) y HyX (andI (order_rel X a1 y) (order_rel X y b1x) Hyla1 Hyub1x)).
We prove the intermediate claim Hyb2: y ∈ b2.
rewrite the current goal using Hb2eq (from left to right).
An exact proof term for the current goal is (SepI X (Îģx0 : set ⇒ order_rel X a0 x0) y HyX Hyla0).
An exact proof term for the current goal is (binintersectI b1 b2 y Hyb1 Hyb2).
Assume Hb1B: b1 ∈ Blow.
Apply (binunionE (Aint âˆĒ Blow) Cup b2 Hb2tri) to the current goal.
Assume Hb2AB: b2 ∈ (Aint âˆĒ Blow).
Apply (binunionE Aint Blow b2 Hb2AB) to the current goal.
Assume Hb2A: b2 ∈ Aint.
We prove the intermediate claim Hexb0: ∃b0 ∈ X, b1 = {x0 ∈ X|order_rel X x0 b0}.
An exact proof term for the current goal is (SepE2 (đ’Ģ X) (ÎģI0 : set ⇒ ∃b0 ∈ X, I0 = {x0 ∈ X|order_rel X x0 b0}) b1 Hb1B).
We prove the intermediate claim Hexab: ∃a1 ∈ X, ∃b1x ∈ X, b2 = {x0 ∈ X|order_rel X a1 x0 ∧ order_rel X x0 b1x}.
An exact proof term for the current goal is (SepE2 (đ’Ģ X) (ÎģI0 : set ⇒ ∃a ∈ X, ∃b ∈ X, I0 = {x0 ∈ X|order_rel X a x0 ∧ order_rel X x0 b}) b2 Hb2A).
Apply Hexb0 to the current goal.
Let b0 be given.
Assume Hb0core: b0 ∈ X ∧ b1 = {x0 ∈ X|order_rel X x0 b0}.
Apply Hb0core to the current goal.
Assume Hb0X: b0 ∈ X.
Assume Hb1eq: b1 = {x0 ∈ X|order_rel X x0 b0}.
Apply Hexab to the current goal.
Let a1 be given.
Assume Ha1core: a1 ∈ X ∧ ∃b1x ∈ X, b2 = {x0 ∈ X|order_rel X a1 x0 ∧ order_rel X x0 b1x}.
Apply Ha1core to the current goal.
Assume Ha1X: a1 ∈ X.
Assume Hexb1x.
Apply Hexb1x to the current goal.
Let b1x be given.
Assume Hb1xcore: b1x ∈ X ∧ b2 = {x0 ∈ X|order_rel X a1 x0 ∧ order_rel X x0 b1x}.
Apply Hb1xcore to the current goal.
Assume Hb1xX: b1x ∈ X.
Assume Hb2eq: b2 = {x0 ∈ X|order_rel X a1 x0 ∧ order_rel X x0 b1x}.
Apply (order_rel_trichotomy_or_impred X b0 b1x Hso Hb0X Hb1xX (∃b3 ∈ (order_topology_basis X), x ∈ b3 ∧ b3 ⊆ b1 ∩ b2)) to the current goal.
Assume Hb0b1x: order_rel X b0 b1x.
Set b3 to be the term {x0 ∈ X|order_rel X a1 x0 ∧ order_rel X x0 b0}.
We use b3 to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim Hb3Pow: b3 ∈ đ’Ģ X.
Apply PowerI to the current goal.
Let y be given.
Assume Hy: y ∈ b3.
An exact proof term for the current goal is (SepE1 X (Îģx0 : set ⇒ order_rel X a1 x0 ∧ order_rel X x0 b0) y Hy).
We prove the intermediate claim Hexab3: ∃a ∈ X, ∃b ∈ X, b3 = {x0 ∈ X|order_rel X a x0 ∧ order_rel X x0 b}.
We use a1 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Ha1X.
We use b0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hb0X.
Use reflexivity.
We prove the intermediate claim Hb3A: b3 ∈ Aint.
An exact proof term for the current goal is (SepI (đ’Ģ X) (ÎģI0 : set ⇒ ∃a ∈ X, ∃b ∈ X, I0 = {x0 ∈ X|order_rel X a x0 ∧ order_rel X x0 b}) b3 Hb3Pow Hexab3).
We prove the intermediate claim Hb3tri: b3 ∈ (Aint âˆĒ Blow âˆĒ Cup).
An exact proof term for the current goal is (binunionI1 (Aint âˆĒ Blow) Cup b3 (binunionI1 Aint Blow b3 Hb3A)).
We prove the intermediate claim Hb3Bold: b3 ∈ Bold.
rewrite the current goal using HBdef (from left to right).
An exact proof term for the current goal is Hb3tri.
An exact proof term for the current goal is (binunionI1 Bold {X} b3 Hb3Bold).
Apply andI to the current goal.
We prove the intermediate claim HxB1: x ∈ {x0 ∈ X|order_rel X x0 b0}.
rewrite the current goal using Hb1eq (from right to left).
An exact proof term for the current goal is Hx1.
We prove the intermediate claim HxB2: x ∈ {x0 ∈ X|order_rel X a1 x0 ∧ order_rel X x0 b1x}.
rewrite the current goal using Hb2eq (from right to left).
An exact proof term for the current goal is Hx2.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (Îģx0 : set ⇒ order_rel X x0 b0) x HxB1).
We prove the intermediate claim Hxrel2: order_rel X a1 x ∧ order_rel X x b1x.
An exact proof term for the current goal is (SepE2 X (Îģx0 : set ⇒ order_rel X a1 x0 ∧ order_rel X x0 b1x) x HxB2).
We prove the intermediate claim Hxa1: order_rel X a1 x.
An exact proof term for the current goal is (andEL (order_rel X a1 x) (order_rel X x b1x) Hxrel2).
We prove the intermediate claim Hxub0: order_rel X x b0.
An exact proof term for the current goal is (SepE2 X (Îģx0 : set ⇒ order_rel X x0 b0) x HxB1).
An exact proof term for the current goal is (SepI X (Îģx0 : set ⇒ order_rel X a1 x0 ∧ order_rel X x0 b0) x HxX (andI (order_rel X a1 x) (order_rel X x b0) Hxa1 Hxub0)).
We will prove b3 ⊆ b1 ∩ b2.
Let y be given.
Assume Hy3: y ∈ b3.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (SepE1 X (Îģx0 : set ⇒ order_rel X a1 x0 ∧ order_rel X x0 b0) y Hy3).
We prove the intermediate claim Hyrel: order_rel X a1 y ∧ order_rel X y b0.
An exact proof term for the current goal is (SepE2 X (Îģx0 : set ⇒ order_rel X a1 x0 ∧ order_rel X x0 b0) y Hy3).
We prove the intermediate claim Hyla1: order_rel X a1 y.
An exact proof term for the current goal is (andEL (order_rel X a1 y) (order_rel X y b0) Hyrel).
We prove the intermediate claim Hyub0: order_rel X y b0.
An exact proof term for the current goal is (andER (order_rel X a1 y) (order_rel X y b0) Hyrel).
We prove the intermediate claim Hyub1x: order_rel X y b1x.
An exact proof term for the current goal is (order_rel_trans X y b0 b1x Hso HyX Hb0X Hb1xX Hyub0 Hb0b1x).
We prove the intermediate claim Hyb1: y ∈ b1.
rewrite the current goal using Hb1eq (from left to right).
An exact proof term for the current goal is (SepI X (Îģx0 : set ⇒ order_rel X x0 b0) y HyX Hyub0).
We prove the intermediate claim Hyb2: y ∈ b2.
rewrite the current goal using Hb2eq (from left to right).
An exact proof term for the current goal is (SepI X (Îģx0 : set ⇒ order_rel X a1 x0 ∧ order_rel X x0 b1x) y HyX (andI (order_rel X a1 y) (order_rel X y b1x) Hyla1 Hyub1x)).
An exact proof term for the current goal is (binintersectI b1 b2 y Hyb1 Hyb2).
Assume Hb_eq: b0 = b1x.
We use b2 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (binunionI1 Bold {X} b2 Hb2old).
Apply andI to the current goal.
An exact proof term for the current goal is Hx2.
We will prove b2 ⊆ b1 ∩ b2.
Let y be given.
Assume Hyb2: y ∈ b2.
We prove the intermediate claim Hyb2Sep: y ∈ {x0 ∈ X|order_rel X a1 x0 ∧ order_rel X x0 b1x}.
rewrite the current goal using Hb2eq (from right to left).
An exact proof term for the current goal is Hyb2.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (SepE1 X (Îģx0 : set ⇒ order_rel X a1 x0 ∧ order_rel X x0 b1x) y Hyb2Sep).
We prove the intermediate claim Hyrel: order_rel X a1 y ∧ order_rel X y b1x.
An exact proof term for the current goal is (SepE2 X (Îģx0 : set ⇒ order_rel X a1 x0 ∧ order_rel X x0 b1x) y Hyb2Sep).
We prove the intermediate claim Hyub1x: order_rel X y b1x.
An exact proof term for the current goal is (andER (order_rel X a1 y) (order_rel X y b1x) Hyrel).
We prove the intermediate claim Hyub0: order_rel X y b0.
rewrite the current goal using Hb_eq (from left to right).
An exact proof term for the current goal is Hyub1x.
We prove the intermediate claim Hyb1: y ∈ b1.
rewrite the current goal using Hb1eq (from left to right).
An exact proof term for the current goal is (SepI X (Îģx0 : set ⇒ order_rel X x0 b0) y HyX Hyub0).
An exact proof term for the current goal is (binintersectI b1 b2 y Hyb1 Hyb2).
Assume Hb1xb0: order_rel X b1x b0.
We use b2 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (binunionI1 Bold {X} b2 Hb2old).
Apply andI to the current goal.
An exact proof term for the current goal is Hx2.
We will prove b2 ⊆ b1 ∩ b2.
Let y be given.
Assume Hyb2: y ∈ b2.
We prove the intermediate claim Hyb2Sep: y ∈ {x0 ∈ X|order_rel X a1 x0 ∧ order_rel X x0 b1x}.
rewrite the current goal using Hb2eq (from right to left).
An exact proof term for the current goal is Hyb2.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (SepE1 X (Îģx0 : set ⇒ order_rel X a1 x0 ∧ order_rel X x0 b1x) y Hyb2Sep).
We prove the intermediate claim Hyrel: order_rel X a1 y ∧ order_rel X y b1x.
An exact proof term for the current goal is (SepE2 X (Îģx0 : set ⇒ order_rel X a1 x0 ∧ order_rel X x0 b1x) y Hyb2Sep).
We prove the intermediate claim Hyub1x: order_rel X y b1x.
An exact proof term for the current goal is (andER (order_rel X a1 y) (order_rel X y b1x) Hyrel).
We prove the intermediate claim Hyub0: order_rel X y b0.
An exact proof term for the current goal is (order_rel_trans X y b1x b0 Hso HyX Hb1xX Hb0X Hyub1x Hb1xb0).
We prove the intermediate claim Hyb1: y ∈ b1.
rewrite the current goal using Hb1eq (from left to right).
An exact proof term for the current goal is (SepI X (Îģx0 : set ⇒ order_rel X x0 b0) y HyX Hyub0).
An exact proof term for the current goal is (binintersectI b1 b2 y Hyb1 Hyb2).
Assume Hb2B: b2 ∈ Blow.
We prove the intermediate claim Hexb0: ∃b0 ∈ X, b1 = {x0 ∈ X|order_rel X x0 b0}.
An exact proof term for the current goal is (SepE2 (đ’Ģ X) (ÎģI0 : set ⇒ ∃b0 ∈ X, I0 = {x0 ∈ X|order_rel X x0 b0}) b1 Hb1B).
We prove the intermediate claim Hexd0: ∃d0 ∈ X, b2 = {x0 ∈ X|order_rel X x0 d0}.
An exact proof term for the current goal is (SepE2 (đ’Ģ X) (ÎģI0 : set ⇒ ∃d0 ∈ X, I0 = {x0 ∈ X|order_rel X x0 d0}) b2 Hb2B).
Apply Hexb0 to the current goal.
Let b0 be given.
Assume Hb0core: b0 ∈ X ∧ b1 = {x0 ∈ X|order_rel X x0 b0}.
Apply Hb0core to the current goal.
Assume Hb0X: b0 ∈ X.
Assume Hb1eq: b1 = {x0 ∈ X|order_rel X x0 b0}.
Apply Hexd0 to the current goal.
Let d0 be given.
Assume Hd0core: d0 ∈ X ∧ b2 = {x0 ∈ X|order_rel X x0 d0}.
Apply Hd0core to the current goal.
Assume Hd0X: d0 ∈ X.
Assume Hb2eq: b2 = {x0 ∈ X|order_rel X x0 d0}.
Apply (order_rel_trichotomy_or_impred X b0 d0 Hso Hb0X Hd0X (∃b3 ∈ (order_topology_basis X), x ∈ b3 ∧ b3 ⊆ b1 ∩ b2)) to the current goal.
Assume Hbd: order_rel X b0 d0.
We use b1 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (binunionI1 Bold {X} b1 Hb1old).
Apply andI to the current goal.
An exact proof term for the current goal is Hx1.
We will prove b1 ⊆ b1 ∩ b2.
Let y be given.
Assume Hy: y ∈ b1.
We will prove y ∈ b1 ∊ b2.
We prove the intermediate claim Hyb1: y ∈ b1.
An exact proof term for the current goal is Hy.
We prove the intermediate claim Hyin: y ∈ {x0 ∈ X|order_rel X x0 b0}.
rewrite the current goal using Hb1eq (from right to left).
An exact proof term for the current goal is Hy.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (SepE1 X (Îģx0 : set ⇒ order_rel X x0 b0) y Hyin).
We prove the intermediate claim Hyrel: order_rel X y b0.
An exact proof term for the current goal is (SepE2 X (Îģx0 : set ⇒ order_rel X x0 b0) y Hyin).
We prove the intermediate claim Hyrel2: order_rel X y d0.
An exact proof term for the current goal is (order_rel_trans X y b0 d0 Hso HyX Hb0X Hd0X Hyrel Hbd).
We prove the intermediate claim Hyb2: y ∈ b2.
rewrite the current goal using Hb2eq (from left to right).
An exact proof term for the current goal is (SepI X (Îģx0 : set ⇒ order_rel X x0 d0) y HyX Hyrel2).
An exact proof term for the current goal is (binintersectI b1 b2 y Hyb1 Hyb2).
Assume Hbeq: b0 = d0.
We use b1 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (binunionI1 Bold {X} b1 Hb1old).
Apply andI to the current goal.
An exact proof term for the current goal is Hx1.
We will prove b1 ⊆ b1 ∩ b2.
Let y be given.
Assume Hy: y ∈ b1.
We will prove y ∈ b1 ∊ b2.
We prove the intermediate claim Hyb1: y ∈ b1.
An exact proof term for the current goal is Hy.
We prove the intermediate claim Hyin: y ∈ {x0 ∈ X|order_rel X x0 b0}.
rewrite the current goal using Hb1eq (from right to left).
An exact proof term for the current goal is Hy.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (SepE1 X (Îģx0 : set ⇒ order_rel X x0 b0) y Hyin).
We prove the intermediate claim Hyrel: order_rel X y b0.
An exact proof term for the current goal is (SepE2 X (Îģx0 : set ⇒ order_rel X x0 b0) y Hyin).
We prove the intermediate claim Hyrel2: order_rel X y d0.
rewrite the current goal using Hbeq (from right to left).
An exact proof term for the current goal is Hyrel.
We prove the intermediate claim Hyb2: y ∈ b2.
rewrite the current goal using Hb2eq (from left to right).
An exact proof term for the current goal is (SepI X (Îģx0 : set ⇒ order_rel X x0 d0) y HyX Hyrel2).
An exact proof term for the current goal is (binintersectI b1 b2 y Hyb1 Hyb2).
Assume Hdb: order_rel X d0 b0.
We use b2 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (binunionI1 Bold {X} b2 Hb2old).
Apply andI to the current goal.
An exact proof term for the current goal is Hx2.
We will prove b2 ⊆ b1 ∩ b2.
Let y be given.
Assume Hy: y ∈ b2.
We will prove y ∈ b1 ∊ b2.
We prove the intermediate claim Hyb2: y ∈ b2.
An exact proof term for the current goal is Hy.
We prove the intermediate claim Hyin: y ∈ {x0 ∈ X|order_rel X x0 d0}.
rewrite the current goal using Hb2eq (from right to left).
An exact proof term for the current goal is Hy.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (SepE1 X (Îģx0 : set ⇒ order_rel X x0 d0) y Hyin).
We prove the intermediate claim Hyrel: order_rel X y d0.
An exact proof term for the current goal is (SepE2 X (Îģx0 : set ⇒ order_rel X x0 d0) y Hyin).
We prove the intermediate claim Hyrel1: order_rel X y b0.
An exact proof term for the current goal is (order_rel_trans X y d0 b0 Hso HyX Hd0X Hb0X Hyrel Hdb).
We prove the intermediate claim Hyb1: y ∈ b1.
rewrite the current goal using Hb1eq (from left to right).
An exact proof term for the current goal is (SepI X (Îģx0 : set ⇒ order_rel X x0 b0) y HyX Hyrel1).
An exact proof term for the current goal is (binintersectI b1 b2 y Hyb1 Hyb2).
Assume Hb2C: b2 ∈ Cup.
We prove the intermediate claim Hexb0: ∃b0 ∈ X, b1 = {x0 ∈ X|order_rel X x0 b0}.
An exact proof term for the current goal is (SepE2 (đ’Ģ X) (ÎģI0 : set ⇒ ∃b0 ∈ X, I0 = {x0 ∈ X|order_rel X x0 b0}) b1 Hb1B).
We prove the intermediate claim Hexa0: ∃a0 ∈ X, b2 = {x0 ∈ X|order_rel X a0 x0}.
An exact proof term for the current goal is (SepE2 (đ’Ģ X) (ÎģI0 : set ⇒ ∃a0 ∈ X, I0 = {x0 ∈ X|order_rel X a0 x0}) b2 Hb2C).
Apply Hexb0 to the current goal.
Let b0 be given.
Assume Hb0core: b0 ∈ X ∧ b1 = {x0 ∈ X|order_rel X x0 b0}.
Apply Hb0core to the current goal.
Assume Hb0X: b0 ∈ X.
Assume Hb1eq: b1 = {x0 ∈ X|order_rel X x0 b0}.
Apply Hexa0 to the current goal.
Let a0 be given.
Assume Ha0core: a0 ∈ X ∧ b2 = {x0 ∈ X|order_rel X a0 x0}.
Apply Ha0core to the current goal.
Assume Ha0X: a0 ∈ X.
Assume Hb2eq: b2 = {x0 ∈ X|order_rel X a0 x0}.
Set b3 to be the term {x0 ∈ X|order_rel X a0 x0 ∧ order_rel X x0 b0}.
We use b3 to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim Hb3Pow: b3 ∈ đ’Ģ X.
Apply PowerI to the current goal.
Let y be given.
Assume Hy: y ∈ b3.
An exact proof term for the current goal is (SepE1 X (Îģx0 : set ⇒ order_rel X a0 x0 ∧ order_rel X x0 b0) y Hy).
We prove the intermediate claim Hexab: ∃a ∈ X, ∃b ∈ X, b3 = {x0 ∈ X|order_rel X a x0 ∧ order_rel X x0 b}.
We use a0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Ha0X.
We use b0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hb0X.
Use reflexivity.
We prove the intermediate claim Hb3A: b3 ∈ Aint.
An exact proof term for the current goal is (SepI (đ’Ģ X) (ÎģI0 : set ⇒ ∃a ∈ X, ∃b ∈ X, I0 = {x0 ∈ X|order_rel X a x0 ∧ order_rel X x0 b}) b3 Hb3Pow Hexab).
We prove the intermediate claim Hb3tri: b3 ∈ (Aint âˆĒ Blow âˆĒ Cup).
An exact proof term for the current goal is (binunionI1 (Aint âˆĒ Blow) Cup b3 (binunionI1 Aint Blow b3 Hb3A)).
We prove the intermediate claim Hb3Bold: b3 ∈ Bold.
rewrite the current goal using HBdef (from left to right).
An exact proof term for the current goal is Hb3tri.
An exact proof term for the current goal is (binunionI1 Bold {X} b3 Hb3Bold).
Apply andI to the current goal.
We prove the intermediate claim HxB1: x ∈ {x0 ∈ X|order_rel X x0 b0}.
rewrite the current goal using Hb1eq (from right to left).
An exact proof term for the current goal is Hx1.
We prove the intermediate claim HxB2: x ∈ {x0 ∈ X|order_rel X a0 x0}.
rewrite the current goal using Hb2eq (from right to left).
An exact proof term for the current goal is Hx2.
We prove the intermediate claim Hrelxb0: order_rel X x b0.
An exact proof term for the current goal is (SepE2 X (Îģx0 : set ⇒ order_rel X x0 b0) x HxB1).
We prove the intermediate claim Hrela0x: order_rel X a0 x.
An exact proof term for the current goal is (SepE2 X (Îģx0 : set ⇒ order_rel X a0 x0) x HxB2).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (Îģx0 : set ⇒ order_rel X a0 x0) x HxB2).
An exact proof term for the current goal is (SepI X (Îģx0 : set ⇒ order_rel X a0 x0 ∧ order_rel X x0 b0) x HxX (andI (order_rel X a0 x) (order_rel X x b0) Hrela0x Hrelxb0)).
We will prove b3 ⊆ b1 ∩ b2.
Let y be given.
Assume Hy3: y ∈ b3.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (SepE1 X (Îģx0 : set ⇒ order_rel X a0 x0 ∧ order_rel X x0 b0) y Hy3).
We prove the intermediate claim Hyrel: order_rel X a0 y ∧ order_rel X y b0.
An exact proof term for the current goal is (SepE2 X (Îģx0 : set ⇒ order_rel X a0 x0 ∧ order_rel X x0 b0) y Hy3).
We prove the intermediate claim Hyrela: order_rel X a0 y.
An exact proof term for the current goal is (andEL (order_rel X a0 y) (order_rel X y b0) Hyrel).
We prove the intermediate claim Hyrelb: order_rel X y b0.
An exact proof term for the current goal is (andER (order_rel X a0 y) (order_rel X y b0) Hyrel).
We prove the intermediate claim Hyb1: y ∈ b1.
rewrite the current goal using Hb1eq (from left to right).
An exact proof term for the current goal is (SepI X (Îģx0 : set ⇒ order_rel X x0 b0) y HyX Hyrelb).
We prove the intermediate claim Hyb2: y ∈ b2.
rewrite the current goal using Hb2eq (from left to right).
An exact proof term for the current goal is (SepI X (Îģx0 : set ⇒ order_rel X a0 x0) y HyX Hyrela).
An exact proof term for the current goal is (binintersectI b1 b2 y Hyb1 Hyb2).
Assume Hb1C: b1 ∈ Cup.
Apply (binunionE (Aint âˆĒ Blow) Cup b2 Hb2tri) to the current goal.
Assume Hb2AB: b2 ∈ (Aint âˆĒ Blow).
Apply (binunionE Aint Blow b2 Hb2AB) to the current goal.
Assume Hb2A: b2 ∈ Aint.
We prove the intermediate claim Hexa0: ∃a0 ∈ X, b1 = {x0 ∈ X|order_rel X a0 x0}.
An exact proof term for the current goal is (SepE2 (đ’Ģ X) (ÎģI0 : set ⇒ ∃a0 ∈ X, I0 = {x0 ∈ X|order_rel X a0 x0}) b1 Hb1C).
We prove the intermediate claim Hexab: ∃a1 ∈ X, ∃b1x ∈ X, b2 = {x0 ∈ X|order_rel X a1 x0 ∧ order_rel X x0 b1x}.
An exact proof term for the current goal is (SepE2 (đ’Ģ X) (ÎģI0 : set ⇒ ∃a ∈ X, ∃b ∈ X, I0 = {x0 ∈ X|order_rel X a x0 ∧ order_rel X x0 b}) b2 Hb2A).
Apply Hexa0 to the current goal.
Let a0 be given.
Assume Ha0core: a0 ∈ X ∧ b1 = {x0 ∈ X|order_rel X a0 x0}.
Apply Ha0core to the current goal.
Assume Ha0X: a0 ∈ X.
Assume Hb1eq: b1 = {x0 ∈ X|order_rel X a0 x0}.
Apply Hexab to the current goal.
Let a1 be given.
Assume Ha1core: a1 ∈ X ∧ ∃b1x ∈ X, b2 = {x0 ∈ X|order_rel X a1 x0 ∧ order_rel X x0 b1x}.
Apply Ha1core to the current goal.
Assume Ha1X: a1 ∈ X.
Assume Hexb1x.
Apply Hexb1x to the current goal.
Let b1x be given.
Assume Hb1xcore: b1x ∈ X ∧ b2 = {x0 ∈ X|order_rel X a1 x0 ∧ order_rel X x0 b1x}.
Apply Hb1xcore to the current goal.
Assume Hb1xX: b1x ∈ X.
Assume Hb2eq: b2 = {x0 ∈ X|order_rel X a1 x0 ∧ order_rel X x0 b1x}.
Apply (order_rel_trichotomy_or_impred X a0 a1 Hso Ha0X Ha1X (∃b3 ∈ (order_topology_basis X), x ∈ b3 ∧ b3 ⊆ b1 ∩ b2)) to the current goal.
Assume Ha0a1: order_rel X a0 a1.
We use b2 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (binunionI1 Bold {X} b2 Hb2old).
Apply andI to the current goal.
An exact proof term for the current goal is Hx2.
We will prove b2 ⊆ b1 ∩ b2.
Let y be given.
Assume Hyb2: y ∈ b2.
We prove the intermediate claim Hyb2Sep: y ∈ {x0 ∈ X|order_rel X a1 x0 ∧ order_rel X x0 b1x}.
rewrite the current goal using Hb2eq (from right to left).
An exact proof term for the current goal is Hyb2.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (SepE1 X (Îģx0 : set ⇒ order_rel X a1 x0 ∧ order_rel X x0 b1x) y Hyb2Sep).
We prove the intermediate claim Hyrel: order_rel X a1 y ∧ order_rel X y b1x.
An exact proof term for the current goal is (SepE2 X (Îģx0 : set ⇒ order_rel X a1 x0 ∧ order_rel X x0 b1x) y Hyb2Sep).
We prove the intermediate claim Hyla1: order_rel X a1 y.
An exact proof term for the current goal is (andEL (order_rel X a1 y) (order_rel X y b1x) Hyrel).
We prove the intermediate claim Hya0: order_rel X a0 y.
An exact proof term for the current goal is (order_rel_trans X a0 a1 y Hso Ha0X Ha1X HyX Ha0a1 Hyla1).
We prove the intermediate claim Hyb1: y ∈ b1.
rewrite the current goal using Hb1eq (from left to right).
An exact proof term for the current goal is (SepI X (Îģx0 : set ⇒ order_rel X a0 x0) y HyX Hya0).
An exact proof term for the current goal is (binintersectI b1 b2 y Hyb1 Hyb2).
Assume Ha01eq: a0 = a1.
We use b2 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (binunionI1 Bold {X} b2 Hb2old).
Apply andI to the current goal.
An exact proof term for the current goal is Hx2.
We will prove b2 ⊆ b1 ∩ b2.
Let y be given.
Assume Hyb2: y ∈ b2.
We prove the intermediate claim Hyb2Sep: y ∈ {x0 ∈ X|order_rel X a1 x0 ∧ order_rel X x0 b1x}.
rewrite the current goal using Hb2eq (from right to left).
An exact proof term for the current goal is Hyb2.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (SepE1 X (Îģx0 : set ⇒ order_rel X a1 x0 ∧ order_rel X x0 b1x) y Hyb2Sep).
We prove the intermediate claim Hyrel: order_rel X a1 y ∧ order_rel X y b1x.
An exact proof term for the current goal is (SepE2 X (Îģx0 : set ⇒ order_rel X a1 x0 ∧ order_rel X x0 b1x) y Hyb2Sep).
We prove the intermediate claim Hyla1: order_rel X a1 y.
An exact proof term for the current goal is (andEL (order_rel X a1 y) (order_rel X y b1x) Hyrel).
We prove the intermediate claim Hyb1: y ∈ b1.
rewrite the current goal using Hb1eq (from left to right).
rewrite the current goal using Ha01eq (from left to right).
An exact proof term for the current goal is (SepI X (Îģx0 : set ⇒ order_rel X a1 x0) y HyX Hyla1).
An exact proof term for the current goal is (binintersectI b1 b2 y Hyb1 Hyb2).
Assume Ha1a0: order_rel X a1 a0.
Set b3 to be the term {x0 ∈ X|order_rel X a0 x0 ∧ order_rel X x0 b1x}.
We use b3 to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim Hb3Pow: b3 ∈ đ’Ģ X.
Apply PowerI to the current goal.
Let y be given.
Assume Hy: y ∈ b3.
An exact proof term for the current goal is (SepE1 X (Îģx0 : set ⇒ order_rel X a0 x0 ∧ order_rel X x0 b1x) y Hy).
We prove the intermediate claim Hexab3: ∃a ∈ X, ∃b ∈ X, b3 = {x0 ∈ X|order_rel X a x0 ∧ order_rel X x0 b}.
We use a0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Ha0X.
We use b1x to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hb1xX.
Use reflexivity.
We prove the intermediate claim Hb3A: b3 ∈ Aint.
An exact proof term for the current goal is (SepI (đ’Ģ X) (ÎģI0 : set ⇒ ∃a ∈ X, ∃b ∈ X, I0 = {x0 ∈ X|order_rel X a x0 ∧ order_rel X x0 b}) b3 Hb3Pow Hexab3).
We prove the intermediate claim Hb3tri: b3 ∈ (Aint âˆĒ Blow âˆĒ Cup).
An exact proof term for the current goal is (binunionI1 (Aint âˆĒ Blow) Cup b3 (binunionI1 Aint Blow b3 Hb3A)).
We prove the intermediate claim Hb3Bold: b3 ∈ Bold.
rewrite the current goal using HBdef (from left to right).
An exact proof term for the current goal is Hb3tri.
An exact proof term for the current goal is (binunionI1 Bold {X} b3 Hb3Bold).
Apply andI to the current goal.
We prove the intermediate claim HxB1: x ∈ {x0 ∈ X|order_rel X a0 x0}.
rewrite the current goal using Hb1eq (from right to left).
An exact proof term for the current goal is Hx1.
We prove the intermediate claim HxB2: x ∈ {x0 ∈ X|order_rel X a1 x0 ∧ order_rel X x0 b1x}.
rewrite the current goal using Hb2eq (from right to left).
An exact proof term for the current goal is Hx2.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (Îģx0 : set ⇒ order_rel X a0 x0) x HxB1).
We prove the intermediate claim Hxa0: order_rel X a0 x.
An exact proof term for the current goal is (SepE2 X (Îģx0 : set ⇒ order_rel X a0 x0) x HxB1).
We prove the intermediate claim Hxrel2: order_rel X a1 x ∧ order_rel X x b1x.
An exact proof term for the current goal is (SepE2 X (Îģx0 : set ⇒ order_rel X a1 x0 ∧ order_rel X x0 b1x) x HxB2).
We prove the intermediate claim Hxb1x: order_rel X x b1x.
An exact proof term for the current goal is (andER (order_rel X a1 x) (order_rel X x b1x) Hxrel2).
An exact proof term for the current goal is (SepI X (Îģx0 : set ⇒ order_rel X a0 x0 ∧ order_rel X x0 b1x) x HxX (andI (order_rel X a0 x) (order_rel X x b1x) Hxa0 Hxb1x)).
We will prove b3 ⊆ b1 ∩ b2.
Let y be given.
Assume Hy3: y ∈ b3.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (SepE1 X (Îģx0 : set ⇒ order_rel X a0 x0 ∧ order_rel X x0 b1x) y Hy3).
We prove the intermediate claim Hyrel: order_rel X a0 y ∧ order_rel X y b1x.
An exact proof term for the current goal is (SepE2 X (Îģx0 : set ⇒ order_rel X a0 x0 ∧ order_rel X x0 b1x) y Hy3).
We prove the intermediate claim Hyla0: order_rel X a0 y.
An exact proof term for the current goal is (andEL (order_rel X a0 y) (order_rel X y b1x) Hyrel).
We prove the intermediate claim Hyub1x: order_rel X y b1x.
An exact proof term for the current goal is (andER (order_rel X a0 y) (order_rel X y b1x) Hyrel).
We prove the intermediate claim Hyla1: order_rel X a1 y.
An exact proof term for the current goal is (order_rel_trans X a1 a0 y Hso Ha1X Ha0X HyX Ha1a0 Hyla0).
We prove the intermediate claim Hyb1: y ∈ b1.
rewrite the current goal using Hb1eq (from left to right).
An exact proof term for the current goal is (SepI X (Îģx0 : set ⇒ order_rel X a0 x0) y HyX Hyla0).
We prove the intermediate claim Hyb2: y ∈ b2.
rewrite the current goal using Hb2eq (from left to right).
An exact proof term for the current goal is (SepI X (Îģx0 : set ⇒ order_rel X a1 x0 ∧ order_rel X x0 b1x) y HyX (andI (order_rel X a1 y) (order_rel X y b1x) Hyla1 Hyub1x)).
An exact proof term for the current goal is (binintersectI b1 b2 y Hyb1 Hyb2).
Assume Hb2B: b2 ∈ Blow.
We prove the intermediate claim Hexa0: ∃a0 ∈ X, b1 = {x0 ∈ X|order_rel X a0 x0}.
An exact proof term for the current goal is (SepE2 (đ’Ģ X) (ÎģI0 : set ⇒ ∃a0 ∈ X, I0 = {x0 ∈ X|order_rel X a0 x0}) b1 Hb1C).
We prove the intermediate claim Hexb0: ∃b0 ∈ X, b2 = {x0 ∈ X|order_rel X x0 b0}.
An exact proof term for the current goal is (SepE2 (đ’Ģ X) (ÎģI0 : set ⇒ ∃b0 ∈ X, I0 = {x0 ∈ X|order_rel X x0 b0}) b2 Hb2B).
Apply Hexa0 to the current goal.
Let a0 be given.
Assume Ha0core: a0 ∈ X ∧ b1 = {x0 ∈ X|order_rel X a0 x0}.
Apply Ha0core to the current goal.
Assume Ha0X: a0 ∈ X.
Assume Hb1eq: b1 = {x0 ∈ X|order_rel X a0 x0}.
Apply Hexb0 to the current goal.
Let b0 be given.
Assume Hb0core: b0 ∈ X ∧ b2 = {x0 ∈ X|order_rel X x0 b0}.
Apply Hb0core to the current goal.
Assume Hb0X: b0 ∈ X.
Assume Hb2eq: b2 = {x0 ∈ X|order_rel X x0 b0}.
Set b3 to be the term {x0 ∈ X|order_rel X a0 x0 ∧ order_rel X x0 b0}.
We use b3 to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim Hb3Pow: b3 ∈ đ’Ģ X.
Apply PowerI to the current goal.
Let y be given.
Assume Hy: y ∈ b3.
An exact proof term for the current goal is (SepE1 X (Îģx0 : set ⇒ order_rel X a0 x0 ∧ order_rel X x0 b0) y Hy).
We prove the intermediate claim Hexab: ∃a ∈ X, ∃b ∈ X, b3 = {x0 ∈ X|order_rel X a x0 ∧ order_rel X x0 b}.
We use a0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Ha0X.
We use b0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hb0X.
Use reflexivity.
We prove the intermediate claim Hb3A: b3 ∈ Aint.
An exact proof term for the current goal is (SepI (đ’Ģ X) (ÎģI0 : set ⇒ ∃a ∈ X, ∃b ∈ X, I0 = {x0 ∈ X|order_rel X a x0 ∧ order_rel X x0 b}) b3 Hb3Pow Hexab).
We prove the intermediate claim Hb3tri: b3 ∈ (Aint âˆĒ Blow âˆĒ Cup).
An exact proof term for the current goal is (binunionI1 (Aint âˆĒ Blow) Cup b3 (binunionI1 Aint Blow b3 Hb3A)).
We prove the intermediate claim Hb3Bold: b3 ∈ Bold.
rewrite the current goal using HBdef (from left to right).
An exact proof term for the current goal is Hb3tri.
An exact proof term for the current goal is (binunionI1 Bold {X} b3 Hb3Bold).
Apply andI to the current goal.
We prove the intermediate claim HxB1: x ∈ {x0 ∈ X|order_rel X a0 x0}.
rewrite the current goal using Hb1eq (from right to left).
An exact proof term for the current goal is Hx1.
We prove the intermediate claim HxB2: x ∈ {x0 ∈ X|order_rel X x0 b0}.
rewrite the current goal using Hb2eq (from right to left).
An exact proof term for the current goal is Hx2.
We prove the intermediate claim Hrela0x: order_rel X a0 x.
An exact proof term for the current goal is (SepE2 X (Îģx0 : set ⇒ order_rel X a0 x0) x HxB1).
We prove the intermediate claim Hrelxb0: order_rel X x b0.
An exact proof term for the current goal is (SepE2 X (Îģx0 : set ⇒ order_rel X x0 b0) x HxB2).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (Îģx0 : set ⇒ order_rel X a0 x0) x HxB1).
An exact proof term for the current goal is (SepI X (Îģx0 : set ⇒ order_rel X a0 x0 ∧ order_rel X x0 b0) x HxX (andI (order_rel X a0 x) (order_rel X x b0) Hrela0x Hrelxb0)).
We will prove b3 ⊆ b1 ∩ b2.
Let y be given.
Assume Hy3: y ∈ b3.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (SepE1 X (Îģx0 : set ⇒ order_rel X a0 x0 ∧ order_rel X x0 b0) y Hy3).
We prove the intermediate claim Hyrel: order_rel X a0 y ∧ order_rel X y b0.
An exact proof term for the current goal is (SepE2 X (Îģx0 : set ⇒ order_rel X a0 x0 ∧ order_rel X x0 b0) y Hy3).
We prove the intermediate claim Hyrela: order_rel X a0 y.
An exact proof term for the current goal is (andEL (order_rel X a0 y) (order_rel X y b0) Hyrel).
We prove the intermediate claim Hyrelb: order_rel X y b0.
An exact proof term for the current goal is (andER (order_rel X a0 y) (order_rel X y b0) Hyrel).
We prove the intermediate claim Hyb1: y ∈ b1.
rewrite the current goal using Hb1eq (from left to right).
An exact proof term for the current goal is (SepI X (Îģx0 : set ⇒ order_rel X a0 x0) y HyX Hyrela).
We prove the intermediate claim Hyb2: y ∈ b2.
rewrite the current goal using Hb2eq (from left to right).
An exact proof term for the current goal is (SepI X (Îģx0 : set ⇒ order_rel X x0 b0) y HyX Hyrelb).
An exact proof term for the current goal is (binintersectI b1 b2 y Hyb1 Hyb2).
Assume Hb2C: b2 ∈ Cup.
We prove the intermediate claim Hexa0: ∃a0 ∈ X, b1 = {x0 ∈ X|order_rel X a0 x0}.
An exact proof term for the current goal is (SepE2 (đ’Ģ X) (ÎģI0 : set ⇒ ∃a0 ∈ X, I0 = {x0 ∈ X|order_rel X a0 x0}) b1 Hb1C).
We prove the intermediate claim Hexc0: ∃c0 ∈ X, b2 = {x0 ∈ X|order_rel X c0 x0}.
An exact proof term for the current goal is (SepE2 (đ’Ģ X) (ÎģI0 : set ⇒ ∃c0 ∈ X, I0 = {x0 ∈ X|order_rel X c0 x0}) b2 Hb2C).
Apply Hexa0 to the current goal.
Let a0 be given.
Assume Ha0core: a0 ∈ X ∧ b1 = {x0 ∈ X|order_rel X a0 x0}.
Apply Ha0core to the current goal.
Assume Ha0X: a0 ∈ X.
Assume Hb1eq: b1 = {x0 ∈ X|order_rel X a0 x0}.
Apply Hexc0 to the current goal.
Let c0 be given.
Assume Hc0core: c0 ∈ X ∧ b2 = {x0 ∈ X|order_rel X c0 x0}.
Apply Hc0core to the current goal.
Assume Hc0X: c0 ∈ X.
Assume Hb2eq: b2 = {x0 ∈ X|order_rel X c0 x0}.
Apply (order_rel_trichotomy_or_impred X a0 c0 Hso Ha0X Hc0X (∃b3 ∈ (order_topology_basis X), x ∈ b3 ∧ b3 ⊆ b1 ∩ b2)) to the current goal.
Assume Hac: order_rel X a0 c0.
We use b2 to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim Hb2tri: b2 ∈ (Aint âˆĒ Blow âˆĒ Cup).
An exact proof term for the current goal is (binunionI2 (Aint âˆĒ Blow) Cup b2 Hb2C).
We prove the intermediate claim Hb2Bold: b2 ∈ Bold.
rewrite the current goal using HBdef (from left to right).
An exact proof term for the current goal is Hb2tri.
An exact proof term for the current goal is (binunionI1 Bold {X} b2 Hb2Bold).
Apply andI to the current goal.
An exact proof term for the current goal is Hx2.
We will prove b2 ⊆ b1 ∩ b2.
Let y be given.
Assume Hyb2: y ∈ b2.
We prove the intermediate claim Hyb2Sep: y ∈ {x0 ∈ X|order_rel X c0 x0}.
rewrite the current goal using Hb2eq (from right to left).
An exact proof term for the current goal is Hyb2.
We prove the intermediate claim Hyc0: order_rel X c0 y.
An exact proof term for the current goal is (SepE2 X (Îģx0 : set ⇒ order_rel X c0 x0) y Hyb2Sep).
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (SepE1 X (Îģx0 : set ⇒ order_rel X c0 x0) y Hyb2Sep).
We prove the intermediate claim Hya0: order_rel X a0 y.
An exact proof term for the current goal is (order_rel_trans X a0 c0 y Hso Ha0X Hc0X HyX Hac Hyc0).
We prove the intermediate claim Hyb1: y ∈ b1.
rewrite the current goal using Hb1eq (from left to right).
An exact proof term for the current goal is (SepI X (Îģx0 : set ⇒ order_rel X a0 x0) y HyX Hya0).
An exact proof term for the current goal is (binintersectI b1 b2 y Hyb1 Hyb2).
Assume H_eq: a0 = c0.
We use b1 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (binunionI1 Bold {X} b1 Hb1old).
Apply andI to the current goal.
An exact proof term for the current goal is Hx1.
We will prove b1 ⊆ b1 ∩ b2.
Let y be given.
Assume Hyb1: y ∈ b1.
We prove the intermediate claim HyX: y ∈ X.
We prove the intermediate claim Hyb1Sep: y ∈ {x0 ∈ X|order_rel X a0 x0}.
rewrite the current goal using Hb1eq (from right to left).
An exact proof term for the current goal is Hyb1.
An exact proof term for the current goal is (SepE1 X (Îģx0 : set ⇒ order_rel X a0 x0) y Hyb1Sep).
We prove the intermediate claim Hya0: order_rel X a0 y.
We prove the intermediate claim Hyb1Sep: y ∈ {x0 ∈ X|order_rel X a0 x0}.
rewrite the current goal using Hb1eq (from right to left).
An exact proof term for the current goal is Hyb1.
An exact proof term for the current goal is (SepE2 X (Îģx0 : set ⇒ order_rel X a0 x0) y Hyb1Sep).
We prove the intermediate claim Hyc0: order_rel X c0 y.
rewrite the current goal using H_eq (from right to left).
An exact proof term for the current goal is Hya0.
We prove the intermediate claim Hyb2: y ∈ b2.
rewrite the current goal using Hb2eq (from left to right).
An exact proof term for the current goal is (SepI X (Îģx0 : set ⇒ order_rel X c0 x0) y HyX Hyc0).
An exact proof term for the current goal is (binintersectI b1 b2 y Hyb1 Hyb2).
Assume Hca: order_rel X c0 a0.
We use b1 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (binunionI1 Bold {X} b1 Hb1old).
Apply andI to the current goal.
An exact proof term for the current goal is Hx1.
We will prove b1 ⊆ b1 ∩ b2.
Let y be given.
Assume Hyb1: y ∈ b1.
We prove the intermediate claim Hya0: order_rel X a0 y.
We prove the intermediate claim Hyb1Sep: y ∈ {x0 ∈ X|order_rel X a0 x0}.
rewrite the current goal using Hb1eq (from right to left).
An exact proof term for the current goal is Hyb1.
An exact proof term for the current goal is (SepE2 X (Îģx0 : set ⇒ order_rel X a0 x0) y Hyb1Sep).
We prove the intermediate claim HyX: y ∈ X.
We prove the intermediate claim Hyb1Sep: y ∈ {x0 ∈ X|order_rel X a0 x0}.
rewrite the current goal using Hb1eq (from right to left).
An exact proof term for the current goal is Hyb1.
An exact proof term for the current goal is (SepE1 X (Îģx0 : set ⇒ order_rel X a0 x0) y Hyb1Sep).
We prove the intermediate claim Hyc0: order_rel X c0 y.
An exact proof term for the current goal is (order_rel_trans X c0 a0 y Hso Hc0X Ha0X HyX Hca Hya0).
We prove the intermediate claim Hyb2: y ∈ b2.
rewrite the current goal using Hb2eq (from left to right).
An exact proof term for the current goal is (SepI X (Îģx0 : set ⇒ order_rel X c0 x0) y HyX Hyc0).
An exact proof term for the current goal is (binintersectI b1 b2 y Hyb1 Hyb2).
Assume Hb2X: b2 ∈ {X}.
We prove the intermediate claim Hb2eq: b2 = X.
An exact proof term for the current goal is (SingE X b2 Hb2X).
rewrite the current goal using Hb2eq (from left to right).
We use b1 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (binunionI1 Bold {X} b1 Hb1old).
Apply andI to the current goal.
An exact proof term for the current goal is Hx1.
We will prove b1 ⊆ b1 ∩ X.
We prove the intermediate claim Hb1Pow: b1 ∈ đ’Ģ X.
An exact proof term for the current goal is (HsubPow b1 (binunionI1 Bold {X} b1 Hb1old)).
We prove the intermediate claim Hb1sub: b1 ⊆ X.
An exact proof term for the current goal is (PowerE X b1 Hb1Pow).
Let y be given.
Assume Hy: y ∈ b1.
An exact proof term for the current goal is (binintersectI b1 X y Hy (Hb1sub y Hy)).
Assume Hb1X: b1 ∈ {X}.
We prove the intermediate claim Hb1eq: b1 = X.
An exact proof term for the current goal is (SingE X b1 Hb1X).
rewrite the current goal using Hb1eq (from left to right).
We use b2 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hb2.
Apply andI to the current goal.
An exact proof term for the current goal is Hx2.
We will prove b2 ⊆ X ∩ b2.
We prove the intermediate claim Hb2Pow: b2 ∈ đ’Ģ X.
An exact proof term for the current goal is (HsubPow b2 Hb2).
We prove the intermediate claim Hb2sub: b2 ⊆ X.
An exact proof term for the current goal is (PowerE X b2 Hb2Pow).
Let y be given.
Assume Hy: y ∈ b2.
An exact proof term for the current goal is (binintersectI X b2 y (Hb2sub y Hy) Hy).
An exact proof term for the current goal is (andI (A ∧ Bcov) Bref Hab Href).
∎