Let X, Tx, A, B, S, Ts, WF, C and pick be given.
Assume Hlin: linear_continuum X Tx.
Assume HAcl: closed_in X Tx A.
Assume HBcl: closed_in X Tx B.
Assume HAB: A ∩ B = Empty.
Assume HSdef: S = X βˆ– (A βˆͺ B).
Assume HTsdef: Ts = subspace_topology X Tx S.
Assume HWFdef: WF = {W0 ∈ 𝒫 S|ex32_8_WFpred X A B S Ts W0}.
Assume HCdef: C = {pick W0|W0 ∈ WF}.
Assume Hpick: βˆ€W : set, W ∈ WF β†’ pick W ∈ W.
We will prove closed_in X Tx C.
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 ∧ (βˆ€A0 : set, A0 βŠ† X β†’ A0 β‰  Empty β†’ (βˆƒupper : set, upper ∈ X ∧ βˆ€a0 : set, a0 ∈ A0 β†’ order_rel X a0 upper ∨ a0 = upper) β†’ βˆƒ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)).
We prove the intermediate claim HT2: T2.
An exact proof term for the current goal is Hlin.
We prove the intermediate claim HT1: T1.
An exact proof term for the current goal is (andEL T1 (βˆ€A0 : set, A0 βŠ† X β†’ A0 β‰  Empty β†’ (βˆƒupper : set, upper ∈ X ∧ βˆ€a0 : set, a0 ∈ A0 β†’ order_rel X a0 upper ∨ a0 = upper) β†’ βˆƒ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)) 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 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).
We prove the intermediate claim HTx: topology_on X Tx.
rewrite the current goal using HTxeq (from left to right).
An exact proof term for the current goal is (order_topology_is_topology X Hso).
Set U to be the term X βˆ– C.
We prove the intermediate claim HCsubX: C βŠ† X.
rewrite the current goal using HCdef (from left to right).
Let c be given.
Assume HcC: c ∈ {pick W0|W0 ∈ WF}.
Apply (ReplE_impred WF (Ξ»W0 : set β‡’ pick W0) c HcC) to the current goal.
Let W0 be given.
Assume HW0WF: W0 ∈ WF.
Assume HcEq: c = pick W0.
We prove the intermediate claim HpickW0: pick W0 ∈ W0.
An exact proof term for the current goal is (Hpick W0 HW0WF).
We prove the intermediate claim HW0WF': W0 ∈ {W1 ∈ 𝒫 S|ex32_8_WFpred X A B S Ts W1}.
rewrite the current goal using HWFdef (from right to left).
An exact proof term for the current goal is HW0WF.
We prove the intermediate claim HW0Pow: W0 ∈ 𝒫 S.
An exact proof term for the current goal is (SepE1 (𝒫 S) (Ξ»W1 : set β‡’ ex32_8_WFpred X A B S Ts W1) W0 HW0WF').
We prove the intermediate claim HW0subS: W0 βŠ† S.
An exact proof term for the current goal is (PowerE S W0 HW0Pow).
We prove the intermediate claim HpickS: pick W0 ∈ S.
An exact proof term for the current goal is (HW0subS (pick W0) HpickW0).
We prove the intermediate claim HSsubX: S βŠ† X.
rewrite the current goal using HSdef (from left to right).
An exact proof term for the current goal is (setminus_Subq X (A βˆͺ B)).
We prove the intermediate claim HpickX: pick W0 ∈ X.
An exact proof term for the current goal is (HSsubX (pick W0) HpickS).
rewrite the current goal using HcEq (from left to right).
An exact proof term for the current goal is HpickX.
We prove the intermediate claim HU: U ∈ Tx.
An exact proof term for the current goal is (ex32_8b_complement_open X Tx A B S Ts WF C pick Hlin HAcl HBcl HAB HSdef HTsdef HWFdef HCdef Hpick).
Apply (closed_inI X Tx C HTx HCsubX) to the current goal.
We use U to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HU.
rewrite the current goal using (setminus_setminus_eq X C HCsubX) (from left to right).
Use reflexivity.
∎