Let X, a1, b1x, a2, b2x, b1, b2 and x be given.
Assume Hso Ha1X Hb1xX Ha2X Hb2xX Hb1def Hb2def Hxb1 Hxb2.
Set I1 to be the term {x0 ∈ X|order_rel X a1 x0 ∧ order_rel X x0 b1x}.
Set I2 to be the term {x0 ∈ X|order_rel X a2 x0 ∧ order_rel X x0 b2x}.
We prove the intermediate claim HxI1: x ∈ I1.
rewrite the current goal using Hb1def (from right to left).
An exact proof term for the current goal is Hxb1.
We prove the intermediate claim HxI2: x ∈ I2.
rewrite the current goal using Hb2def (from right to left).
An exact proof term for the current goal is 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 a1 x0 ∧ order_rel X x0 b1x) x HxI1).
We prove the intermediate claim HxI1prop: 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 HxI1).
We prove the intermediate claim Ha1x: 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) HxI1prop).
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) HxI1prop).
We prove the intermediate claim HxI2prop: order_rel X a2 x ∧ order_rel X x b2x.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X a2 x0 ∧ order_rel X x0 b2x) x HxI2).
We prove the intermediate claim Ha2x: order_rel X a2 x.
An exact proof term for the current goal is (andEL (order_rel X a2 x) (order_rel X x b2x) HxI2prop).
We prove the intermediate claim Hxb2x: order_rel X x b2x.
An exact proof term for the current goal is (andER (order_rel X a2 x) (order_rel X x b2x) HxI2prop).
We prove the intermediate claim Hexa: ∃a3 ∈ X, (a3 = a1 ∨ a3 = a2) ∧ (order_rel X a3 x ∧ ((a1 = a3 ∨ order_rel X a1 a3) ∧ (a2 = a3 ∨ order_rel X a2 a3))).
Apply (order_rel_trichotomy_or_impred X a1 a2 Hso Ha1X Ha2X (∃a3 ∈ X, (a3 = a1 ∨ a3 = a2) ∧ (order_rel X a3 x ∧ ((a1 = a3 ∨ order_rel X a1 a3) ∧ (a2 = a3 ∨ order_rel X a2 a3))))) to the current goal.
Assume Ha12: order_rel X a1 a2.
We use a2 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Ha2X.
Apply andI to the current goal.
We will prove a2 = a1 ∨ a2 = a2.
Apply orIR to the current goal.
Use reflexivity.
Apply andI to the current goal.
An exact proof term for the current goal is Ha2x.
Apply andI to the current goal.
We will prove a1 = a2 ∨ order_rel X a1 a2.
Apply orIR to the current goal.
An exact proof term for the current goal is Ha12.
We will prove a2 = a2 ∨ order_rel X a2 a2.
Apply orIL to the current goal.
Use reflexivity.
Assume Haeq: a1 = a2.
We use a1 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Ha1X.
Apply andI to the current goal.
We will prove a1 = a1 ∨ a1 = a2.
Apply orIL to the current goal.
Use reflexivity.
Apply andI to the current goal.
An exact proof term for the current goal is Ha1x.
Apply andI to the current goal.
We will prove a1 = a1 ∨ order_rel X a1 a1.
Apply orIL to the current goal.
Use reflexivity.
We will prove a2 = a1 ∨ order_rel X a2 a1.
Apply orIL to the current goal.
rewrite the current goal using Haeq (from right to left).
Use reflexivity.
Assume Ha21: order_rel X a2 a1.
We use a1 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Ha1X.
Apply andI to the current goal.
We will prove a1 = a1 ∨ a1 = a2.
Apply orIL to the current goal.
Use reflexivity.
Apply andI to the current goal.
An exact proof term for the current goal is Ha1x.
Apply andI to the current goal.
We will prove a1 = a1 ∨ order_rel X a1 a1.
Apply orIL to the current goal.
Use reflexivity.
We will prove a2 = a1 ∨ order_rel X a2 a1.
Apply orIR to the current goal.
An exact proof term for the current goal is Ha21.
Apply Hexa to the current goal.
Let a3 be given.
Assume Ha3pack.
Apply Ha3pack to the current goal.
Assume Ha3X Ha3core.
We prove the intermediate claim Ha3x_and_max: order_rel X a3 x ∧ ((a1 = a3 ∨ order_rel X a1 a3) ∧ (a2 = a3 ∨ order_rel X a2 a3)).
An exact proof term for the current goal is (andER (a3 = a1 ∨ a3 = a2) (order_rel X a3 x ∧ ((a1 = a3 ∨ order_rel X a1 a3) ∧ (a2 = a3 ∨ order_rel X a2 a3))) Ha3core).
We prove the intermediate claim Ha3x: order_rel X a3 x.
An exact proof term for the current goal is (andEL (order_rel X a3 x) ((a1 = a3 ∨ order_rel X a1 a3) ∧ (a2 = a3 ∨ order_rel X a2 a3)) Ha3x_and_max).
We prove the intermediate claim Ha_max: (a1 = a3 ∨ order_rel X a1 a3) ∧ (a2 = a3 ∨ order_rel X a2 a3).
An exact proof term for the current goal is (andER (order_rel X a3 x) ((a1 = a3 ∨ order_rel X a1 a3) ∧ (a2 = a3 ∨ order_rel X a2 a3)) Ha3x_and_max).
We prove the intermediate claim Ha1le: a1 = a3 ∨ order_rel X a1 a3.
An exact proof term for the current goal is (andEL (a1 = a3 ∨ order_rel X a1 a3) (a2 = a3 ∨ order_rel X a2 a3) Ha_max).
We prove the intermediate claim Ha2le: a2 = a3 ∨ order_rel X a2 a3.
An exact proof term for the current goal is (andER (a1 = a3 ∨ order_rel X a1 a3) (a2 = a3 ∨ order_rel X a2 a3) Ha_max).
We prove the intermediate claim Hexb: ∃b3x ∈ X, (b3x = b1x ∨ b3x = b2x) ∧ (order_rel X x b3x ∧ ((b3x = b1x ∨ order_rel X b3x b1x) ∧ (b3x = b2x ∨ order_rel X b3x b2x))).
Apply (order_rel_trichotomy_or_impred X b1x b2x Hso Hb1xX Hb2xX (∃b3x ∈ X, (b3x = b1x ∨ b3x = b2x) ∧ (order_rel X x b3x ∧ ((b3x = b1x ∨ order_rel X b3x b1x) ∧ (b3x = b2x ∨ order_rel X b3x b2x))))) to the current goal.
Assume Hb12: order_rel X b1x b2x.
We use b1x to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hb1xX.
Apply andI to the current goal.
We will prove b1x = b1x ∨ b1x = b2x.
Apply orIL to the current goal.
Use reflexivity.
Apply andI to the current goal.
An exact proof term for the current goal is Hxb1x.
Apply andI to the current goal.
We will prove b1x = b1x ∨ order_rel X b1x b1x.
Apply orIL to the current goal.
Use reflexivity.
We will prove b1x = b2x ∨ order_rel X b1x b2x.
Apply orIR to the current goal.
An exact proof term for the current goal is Hb12.
Assume Hbeq: b1x = b2x.
We use b1x to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hb1xX.
Apply andI to the current goal.
We will prove b1x = b1x ∨ b1x = b2x.
Apply orIL to the current goal.
Use reflexivity.
Apply andI to the current goal.
An exact proof term for the current goal is Hxb1x.
Apply andI to the current goal.
We will prove b1x = b1x ∨ order_rel X b1x b1x.
Apply orIL to the current goal.
Use reflexivity.
We will prove b1x = b2x ∨ order_rel X b1x b2x.
Apply orIL to the current goal.
An exact proof term for the current goal is Hbeq.
Assume Hb21: order_rel X b2x b1x.
We use b2x to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hb2xX.
Apply andI to the current goal.
We will prove b2x = b1x ∨ b2x = b2x.
Apply orIR to the current goal.
Use reflexivity.
Apply andI to the current goal.
An exact proof term for the current goal is Hxb2x.
Apply andI to the current goal.
We will prove b2x = b1x ∨ order_rel X b2x b1x.
Apply orIR to the current goal.
An exact proof term for the current goal is Hb21.
We will prove b2x = b2x ∨ order_rel X b2x b2x.
Apply orIL to the current goal.
Use reflexivity.
Apply Hexb to the current goal.
Let b3x be given.
Assume Hb3pack.
Apply Hb3pack to the current goal.
Assume Hb3xX Hb3core.
We prove the intermediate claim Hxb3x_and_min: order_rel X x b3x ∧ ((b3x = b1x ∨ order_rel X b3x b1x) ∧ (b3x = b2x ∨ order_rel X b3x b2x)).
An exact proof term for the current goal is (andER (b3x = b1x ∨ b3x = b2x) (order_rel X x b3x ∧ ((b3x = b1x ∨ order_rel X b3x b1x) ∧ (b3x = b2x ∨ order_rel X b3x b2x))) Hb3core).
We prove the intermediate claim Hxb3x: order_rel X x b3x.
An exact proof term for the current goal is (andEL (order_rel X x b3x) ((b3x = b1x ∨ order_rel X b3x b1x) ∧ (b3x = b2x ∨ order_rel X b3x b2x)) Hxb3x_and_min).
We prove the intermediate claim Hb_min: (b3x = b1x ∨ order_rel X b3x b1x) ∧ (b3x = b2x ∨ order_rel X b3x b2x).
An exact proof term for the current goal is (andER (order_rel X x b3x) ((b3x = b1x ∨ order_rel X b3x b1x) ∧ (b3x = b2x ∨ order_rel X b3x b2x)) Hxb3x_and_min).
We prove the intermediate claim Hb1ge: b3x = b1x ∨ order_rel X b3x b1x.
An exact proof term for the current goal is (andEL (b3x = b1x ∨ order_rel X b3x b1x) (b3x = b2x ∨ order_rel X b3x b2x) Hb_min).
We prove the intermediate claim Hb2ge: b3x = b2x ∨ order_rel X b3x b2x.
An exact proof term for the current goal is (andER (b3x = b1x ∨ order_rel X b3x b1x) (b3x = b2x ∨ order_rel X b3x b2x) Hb_min).
Set b3 to be the term {x0 ∈ X|order_rel X a3 x0 ∧ order_rel X x0 b3x}.
We prove the intermediate claim Hb3basis: b3 ∈ order_topology_basis X.
We will prove b3 ∈ (({I ∈ 𝒫 X|∃a ∈ X, ∃b ∈ X, I = {x0 ∈ X|order_rel X a x0 ∧ order_rel X x0 b}} ∪ {I ∈ 𝒫 X|∃b ∈ X, I = {x0 ∈ X|order_rel X x0 b}} ∪ {I ∈ 𝒫 X|∃a ∈ X, I = {x0 ∈ X|order_rel X a x0}}) ∪ {X}).
Apply binunionI1 to the current goal.
Apply binunionI1 to the current goal.
Apply binunionI1 to the current goal.
We will prove b3 ∈ {I ∈ 𝒫 X|∃a ∈ X, ∃b ∈ X, I = {x0 ∈ X|order_rel X a x0 ∧ order_rel X x0 b}}.
Apply (SepI (𝒫 X) (λI : set ⇒ ∃a ∈ X, ∃b ∈ X, I = {x0 ∈ X|order_rel X a x0 ∧ order_rel X x0 b}) b3) to the current goal.
We will prove b3 ∈ 𝒫 X.
Apply (PowerI X b3) 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 a3 x0 ∧ order_rel X x0 b3x) y Hy).
We use a3 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Ha3X.
We use b3x to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hb3xX.
Use reflexivity.
We prove the intermediate claim HxInb3: x ∈ b3.
Apply (SepI X (λx0 : set ⇒ order_rel X a3 x0 ∧ order_rel X x0 b3x) x HxX) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Ha3x.
An exact proof term for the current goal is Hxb3x.
We use b3 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hb3basis.
Apply andI to the current goal.
An exact proof term for the current goal is HxInb3.
We will prove b3 ⊆ b1 ∩ b2.
Let y be given.
Assume Hy: 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 a3 x0 ∧ order_rel X x0 b3x) y Hy).
We prove the intermediate claim Hyprop: order_rel X a3 y ∧ order_rel X y b3x.
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ order_rel X a3 x0 ∧ order_rel X x0 b3x) y Hy).
We prove the intermediate claim Ha3y: order_rel X a3 y.
An exact proof term for the current goal is (andEL (order_rel X a3 y) (order_rel X y b3x) Hyprop).
We prove the intermediate claim Hyb3x: order_rel X y b3x.
An exact proof term for the current goal is (andER (order_rel X a3 y) (order_rel X y b3x) Hyprop).
We prove the intermediate claim Ha1y: order_rel X a1 y.
Apply (Ha1le (order_rel X a1 y)) to the current goal.
Assume Ha1eq: a1 = a3.
rewrite the current goal using Ha1eq (from left to right).
An exact proof term for the current goal is Ha3y.
Assume Ha1a3: order_rel X a1 a3.
An exact proof term for the current goal is (order_rel_trans X a1 a3 y Hso Ha1X Ha3X HyX Ha1a3 Ha3y).
We prove the intermediate claim Ha2y: order_rel X a2 y.
Apply (Ha2le (order_rel X a2 y)) to the current goal.
Assume Ha2eq: a2 = a3.
rewrite the current goal using Ha2eq (from left to right).
An exact proof term for the current goal is Ha3y.
Assume Ha2a3: order_rel X a2 a3.
An exact proof term for the current goal is (order_rel_trans X a2 a3 y Hso Ha2X Ha3X HyX Ha2a3 Ha3y).
We prove the intermediate claim Hyb1x: order_rel X y b1x.
Apply (Hb1ge (order_rel X y b1x)) to the current goal.
Assume Hb3eqb1: b3x = b1x.
rewrite the current goal using Hb3eqb1 (from right to left).
An exact proof term for the current goal is Hyb3x.
Assume Hb3ltb1: order_rel X b3x b1x.
An exact proof term for the current goal is (order_rel_trans X y b3x b1x Hso HyX Hb3xX Hb1xX Hyb3x Hb3ltb1).
We prove the intermediate claim Hyb2x: order_rel X y b2x.
Apply (Hb2ge (order_rel X y b2x)) to the current goal.
Assume Hb3eqb2: b3x = b2x.
rewrite the current goal using Hb3eqb2 (from right to left).
An exact proof term for the current goal is Hyb3x.
Assume Hb3ltb2: order_rel X b3x b2x.
An exact proof term for the current goal is (order_rel_trans X y b3x b2x Hso HyX Hb3xX Hb2xX Hyb3x Hb3ltb2).
We prove the intermediate claim Hyb1: y ∈ b1.
rewrite the current goal using Hb1def (from left to right).
Apply (SepI X (λx0 : set ⇒ order_rel X a1 x0 ∧ order_rel X x0 b1x) y HyX) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Ha1y.
An exact proof term for the current goal is Hyb1x.
We prove the intermediate claim Hyb2: y ∈ b2.
rewrite the current goal using Hb2def (from left to right).
Apply (SepI X (λx0 : set ⇒ order_rel X a2 x0 ∧ order_rel X x0 b2x) y HyX) to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is Ha2y.
An exact proof term for the current goal is Hyb2x.
An exact proof term for the current goal is (binintersectI b1 b2 y Hyb1 Hyb2).
∎