Let X and Tx be given.
Assume Hpara: paracompact_space X Tx.
Assume HH: Hausdorff_space X Tx.
We will prove normal_space X Tx.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (andEL (topology_on X Tx) (∀U : set, open_cover X Tx U → ∃V : set, open_cover X Tx V ∧ locally_finite_family X Tx V ∧ refine_of V U) Hpara).
We prove the intermediate claim HT1: one_point_sets_closed X Tx.
We will prove topology_on X Tx ∧ ∀x : set, x ∈ X → closed_in X Tx {x}.
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
Let x be given.
Assume HxX: x ∈ X.
An exact proof term for the current goal is (Hausdorff_singletons_closed X Tx x HH HxX).
We will prove one_point_sets_closed X Tx ∧ ∀A B : set, closed_in X Tx A → closed_in X Tx B → A ∩ B = Empty → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ A ⊆ U ∧ B ⊆ V ∧ U ∩ V = Empty.
Apply andI to the current goal.
An exact proof term for the current goal is HT1.
Let A and B be given.
Assume HAcl: closed_in X Tx A.
Assume HBcl: closed_in X Tx B.
Assume Hdisj: A ∩ B = Empty.
We will prove ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ A ⊆ U ∧ B ⊆ V ∧ U ∩ V = Empty.
We prove the intermediate claim Hreg: regular_space X Tx.
An exact proof term for the current goal is (paracompact_Hausdorff_regular X Tx Hpara HH).
We prove the intermediate claim HregSep: ∀x : set, x ∈ X → ∀F : set, closed_in X Tx F → x ∉ F → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ x ∈ U ∧ F ⊆ V ∧ U ∩ V = Empty.
An exact proof term for the current goal is (andER (one_point_sets_closed X Tx) (∀x : set, x ∈ X → ∀F : set, closed_in X Tx F → x ∉ F → ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ x ∈ U ∧ F ⊆ V ∧ U ∩ V = Empty) Hreg).
We prove the intermediate claim HAsubX: A ⊆ X.
An exact proof term for the current goal is (closed_in_subset X Tx A HAcl).
We prove the intermediate claim HBsubX: B ⊆ X.
An exact proof term for the current goal is (closed_in_subset X Tx B HBcl).
Set sepU to be the term λa : set ⇒ Eps_i (λU : set ⇒ ∃V : set, U ∈ Tx ∧ V ∈ Tx ∧ a ∈ U ∧ B ⊆ V ∧ U ∩ V = Empty).
Set sepV to be the term λa : set ⇒ Eps_i (λV : set ⇒ (sepU a) ∈ Tx ∧ V ∈ Tx ∧ a ∈ (sepU a) ∧ B ⊆ V ∧ (sepU a) ∩ V = Empty).
We prove the intermediate claim HsepProp: ∀a : set, a ∈ A → (sepU a) ∈ Tx ∧ (sepV a) ∈ Tx ∧ a ∈ (sepU a) ∧ B ⊆ (sepV a) ∧ (sepU a) ∩ (sepV a) = Empty.
Let a be given.
Assume HaA: a ∈ A.
We prove the intermediate claim HaX: a ∈ X.
An exact proof term for the current goal is (HAsubX a HaA).
We prove the intermediate claim HaNotB: a ∉ B.
Assume HaB: a ∈ B.
We will prove False.
We prove the intermediate claim HaAB: a ∈ A ∩ B.
An exact proof term for the current goal is (binintersectI A B a HaA HaB).
We prove the intermediate claim HaEmpty: a ∈ Empty.
rewrite the current goal using Hdisj (from right to left).
An exact proof term for the current goal is HaAB.
An exact proof term for the current goal is ((EmptyE a) HaEmpty).
We prove the intermediate claim HexSep: ∃U V : set, U ∈ Tx ∧ V ∈ Tx ∧ a ∈ U ∧ B ⊆ V ∧ U ∩ V = Empty.
An exact proof term for the current goal is (HregSep a HaX B HBcl HaNotB).
We prove the intermediate claim HexU: ∃U : set, ∃V : set, U ∈ Tx ∧ V ∈ Tx ∧ a ∈ U ∧ B ⊆ V ∧ U ∩ V = Empty.
An exact proof term for the current goal is HexSep.
We prove the intermediate claim HsepUex: ∃V : set, (sepU a) ∈ Tx ∧ V ∈ Tx ∧ a ∈ (sepU a) ∧ B ⊆ V ∧ (sepU a) ∩ V = Empty.
An exact proof term for the current goal is (Eps_i_ex (λU : set ⇒ ∃V : set, U ∈ Tx ∧ V ∈ Tx ∧ a ∈ U ∧ B ⊆ V ∧ U ∩ V = Empty) HexU).
We prove the intermediate claim HexV: ∃V : set, (sepU a) ∈ Tx ∧ V ∈ Tx ∧ a ∈ (sepU a) ∧ B ⊆ V ∧ (sepU a) ∩ V = Empty.
An exact proof term for the current goal is HsepUex.
An exact proof term for the current goal is (Eps_i_ex (λV : set ⇒ (sepU a) ∈ Tx ∧ V ∈ Tx ∧ a ∈ (sepU a) ∧ B ⊆ V ∧ (sepU a) ∩ V = Empty) HexV).
Set U0 to be the term X ∖ A.
We prove the intermediate claim HU0Tx: U0 ∈ Tx.
We prove the intermediate claim HU0open: open_in X Tx U0.
An exact proof term for the current goal is (open_of_closed_complement X Tx A HAcl).
An exact proof term for the current goal is (open_in_elem X Tx U0 HU0open).
Set UFam to be the term {sepU a|a ∈ A}.
Set Cover to be the term {U0} ∪ UFam.
We prove the intermediate claim HCoverOpen: ∀u : set, u ∈ Cover → u ∈ Tx.
Let u be given.
Assume Hu: u ∈ Cover.
We will prove u ∈ Tx.
Apply (binunionE' {U0} UFam u (u ∈ Tx)) to the current goal.
Assume Hu0: u ∈ {U0}.
We prove the intermediate claim Hueq: u = U0.
An exact proof term for the current goal is (SingE U0 u Hu0).
rewrite the current goal using Hueq (from left to right).
An exact proof term for the current goal is HU0Tx.
Assume HuU: u ∈ UFam.
Apply (ReplE_impred A (λa : set ⇒ sepU a) u HuU (u ∈ Tx)) to the current goal.
Let a be given.
Assume HaA: a ∈ A.
Assume Hueq: u = sepU a.
We prove the intermediate claim Hsep: (sepU a) ∈ Tx ∧ (sepV a) ∈ Tx ∧ a ∈ (sepU a) ∧ B ⊆ (sepV a) ∧ (sepU a) ∩ (sepV a) = Empty.
An exact proof term for the current goal is (HsepProp a HaA).
rewrite the current goal using Hueq (from left to right).
We prove the intermediate claim Hpqrs: (((sepU a) ∈ Tx ∧ (sepV a) ∈ Tx) ∧ a ∈ (sepU a)) ∧ B ⊆ (sepV a).
An exact proof term for the current goal is (andEL ((((sepU a) ∈ Tx ∧ (sepV a) ∈ Tx) ∧ a ∈ (sepU a)) ∧ B ⊆ (sepV a)) ((sepU a) ∩ (sepV a) = Empty) Hsep).
We prove the intermediate claim Hpqr: ((sepU a) ∈ Tx ∧ (sepV a) ∈ Tx) ∧ a ∈ (sepU a).
An exact proof term for the current goal is (andEL (((sepU a) ∈ Tx ∧ (sepV a) ∈ Tx) ∧ a ∈ (sepU a)) (B ⊆ (sepV a)) Hpqrs).
We prove the intermediate claim Hpq: (sepU a) ∈ Tx ∧ (sepV a) ∈ Tx.
An exact proof term for the current goal is (andEL ((sepU a) ∈ Tx ∧ (sepV a) ∈ Tx) (a ∈ (sepU a)) Hpqr).
An exact proof term for the current goal is (andEL ((sepU a) ∈ Tx) ((sepV a) ∈ Tx) Hpq).
An exact proof term for the current goal is Hu.
We prove the intermediate claim HCoverCovers: covers X Cover.
Let x be given.
Assume HxX: x ∈ X.
Apply (xm (x ∈ A)) to the current goal.
Assume HxA: x ∈ A.
We use (sepU x) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (binunionI2 {U0} UFam (sepU x) (ReplI A (λa : set ⇒ sepU a) x HxA)).
We prove the intermediate claim Hsep: (sepU x) ∈ Tx ∧ (sepV x) ∈ Tx ∧ x ∈ (sepU x) ∧ B ⊆ (sepV x) ∧ (sepU x) ∩ (sepV x) = Empty.
An exact proof term for the current goal is (HsepProp x HxA).
We prove the intermediate claim Hpqrs: (((sepU x) ∈ Tx ∧ (sepV x) ∈ Tx) ∧ x ∈ (sepU x)) ∧ B ⊆ (sepV x).
An exact proof term for the current goal is (andEL ((((sepU x) ∈ Tx ∧ (sepV x) ∈ Tx) ∧ x ∈ (sepU x)) ∧ B ⊆ (sepV x)) ((sepU x) ∩ (sepV x) = Empty) Hsep).
We prove the intermediate claim Hpqr: ((sepU x) ∈ Tx ∧ (sepV x) ∈ Tx) ∧ x ∈ (sepU x).
An exact proof term for the current goal is (andEL (((sepU x) ∈ Tx ∧ (sepV x) ∈ Tx) ∧ x ∈ (sepU x)) (B ⊆ (sepV x)) Hpqrs).
An exact proof term for the current goal is (andER ((sepU x) ∈ Tx ∧ (sepV x) ∈ Tx) (x ∈ (sepU x)) Hpqr).
Assume HxNotA: ¬ (x ∈ A).
We use U0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (binunionI1 {U0} UFam U0 (SingI U0)).
An exact proof term for the current goal is (setminusI X A x HxX HxNotA).
We prove the intermediate claim Hcover: open_cover X Tx Cover.
An exact proof term for the current goal is (andI (∀u : set, u ∈ Cover → u ∈ Tx) (covers X Cover) HCoverOpen HCoverCovers).
We prove the intermediate claim HparaFor: ∀U : set, open_cover X Tx U → ∃W : set, open_cover X Tx W ∧ locally_finite_family X Tx W ∧ refine_of W U.
An exact proof term for the current goal is (andER (topology_on X Tx) (∀U : set, open_cover X Tx U → ∃V : set, open_cover X Tx V ∧ locally_finite_family X Tx V ∧ refine_of V U) Hpara).
We prove the intermediate claim Href: ∃W : set, open_cover X Tx W ∧ locally_finite_family X Tx W ∧ refine_of W Cover.
An exact proof term for the current goal is (HparaFor Cover Hcover).
Apply Href to the current goal.
Let W be given.
Assume HW: open_cover X Tx W ∧ locally_finite_family X Tx W ∧ refine_of W Cover.
Set WF to be the term {w ∈ W|w ∩ A ≠ Empty}.
Set U to be the term ⋃ WF.
We prove the intermediate claim HWpair: open_cover X Tx W ∧ locally_finite_family X Tx W.
An exact proof term for the current goal is (andEL (open_cover X Tx W ∧ locally_finite_family X Tx W) (refine_of W Cover) HW).
We prove the intermediate claim HWref: refine_of W Cover.
An exact proof term for the current goal is (andER (open_cover X Tx W ∧ locally_finite_family X Tx W) (refine_of W Cover) HW).
We prove the intermediate claim HWcover: open_cover X Tx W.
An exact proof term for the current goal is (andEL (open_cover X Tx W) (locally_finite_family X Tx W) HWpair).
We prove the intermediate claim HLFW: locally_finite_family X Tx W.
An exact proof term for the current goal is (andER (open_cover X Tx W) (locally_finite_family X Tx W) HWpair).
We prove the intermediate claim HWopen: ∀w : set, w ∈ W → w ∈ Tx.
An exact proof term for the current goal is (andEL (∀w : set, w ∈ W → w ∈ Tx) (covers X W) HWcover).
We prove the intermediate claim HWcovers: covers X W.
An exact proof term for the current goal is (andER (∀w : set, w ∈ W → w ∈ Tx) (covers X W) HWcover).
We prove the intermediate claim HWFsubW: WF ⊆ W.
An exact proof term for the current goal is (Sep_Subq W (λw : set ⇒ w ∩ A ≠ Empty)).
We prove the intermediate claim HLF_WF: locally_finite_family X Tx WF.
An exact proof term for the current goal is (locally_finite_subfamily X Tx W WF HLFW HWFsubW).
We prove the intermediate claim HWFsubTx: WF ⊆ Tx.
Let w be given.
Assume HwWF: w ∈ WF.
We prove the intermediate claim HwW: w ∈ W.
An exact proof term for the current goal is (SepE1 W (λw0 : set ⇒ w0 ∩ A ≠ Empty) w HwWF).
An exact proof term for the current goal is (HWopen w HwW).
We prove the intermediate claim HUTx: U ∈ Tx.
An exact proof term for the current goal is (topology_union_closed X Tx WF HTx HWFsubTx).
We prove the intermediate claim HUsupX: U ⊆ X.
Let z be given.
Assume HzU: z ∈ U.
Apply (UnionE_impred WF z HzU) to the current goal.
Let w be given.
Assume Hzw: z ∈ w.
Assume HwWF: w ∈ WF.
We prove the intermediate claim HwTx: w ∈ Tx.
An exact proof term for the current goal is (HWFsubTx w HwWF).
We prove the intermediate claim HwsubX: w ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx w HTx HwTx).
An exact proof term for the current goal is (HwsubX z Hzw).
We prove the intermediate claim HAsubU: A ⊆ U.
Let a be given.
Assume HaA: a ∈ A.
We will prove a ∈ U.
We prove the intermediate claim HaX: a ∈ X.
An exact proof term for the current goal is (HAsubX a HaA).
Apply (HWcovers a HaX) to the current goal.
Let w be given.
Assume Hw: w ∈ W ∧ a ∈ w.
We prove the intermediate claim HwW: w ∈ W.
An exact proof term for the current goal is (andEL (w ∈ W) (a ∈ w) Hw).
We prove the intermediate claim Haw: a ∈ w.
An exact proof term for the current goal is (andER (w ∈ W) (a ∈ w) Hw).
We prove the intermediate claim HwAne: w ∩ A ≠ Empty.
An exact proof term for the current goal is (elem_implies_nonempty (w ∩ A) a (binintersectI w A a Haw HaA)).
We prove the intermediate claim HwWF: w ∈ WF.
An exact proof term for the current goal is (SepI W (λw0 : set ⇒ w0 ∩ A ≠ Empty) w HwW HwAne).
An exact proof term for the current goal is (UnionI WF a w Haw HwWF).
Set ClWF to be the term {closure_of X Tx w|w ∈ WF}.
Set C to be the term ⋃ ClWF.
We prove the intermediate claim HWFsubX: ∀w : set, w ∈ WF → w ⊆ X.
Let w be given.
Assume HwWF: w ∈ WF.
We prove the intermediate claim HwTx: w ∈ Tx.
An exact proof term for the current goal is (HWFsubTx w HwWF).
An exact proof term for the current goal is (topology_elem_subset X Tx w HTx HwTx).
We prove the intermediate claim HUdef: U = ⋃ WF.
Use reflexivity.
We prove the intermediate claim HclUsubC': closure_of X Tx (⋃ WF) ⊆ C.
An exact proof term for the current goal is (closure_Union_locally_finite_subset_Union_closures X Tx WF HWFsubX HLF_WF).
We prove the intermediate claim HclUsubC: closure_of X Tx U ⊆ C.
rewrite the current goal using HUdef (from left to right).
An exact proof term for the current goal is HclUsubC'.
We prove the intermediate claim HCsubclU: C ⊆ closure_of X Tx U.
Let z be given.
Assume HzC: z ∈ C.
We will prove z ∈ closure_of X Tx U.
Apply (UnionE_impred ClWF z HzC) to the current goal.
Let clw be given.
Assume Hzclw: z ∈ clw.
Assume Hclw: clw ∈ ClWF.
Apply (ReplE_impred WF (λw : set ⇒ closure_of X Tx w) clw Hclw) to the current goal.
Let w be given.
Assume HwWF: w ∈ WF.
Assume Hclweq: clw = closure_of X Tx w.
We prove the intermediate claim Hzclw2: z ∈ closure_of X Tx w.
rewrite the current goal using Hclweq (from right to left).
An exact proof term for the current goal is Hzclw.
We prove the intermediate claim HwsubU: w ⊆ U.
Let t be given.
Assume Htw: t ∈ w.
An exact proof term for the current goal is (UnionI WF t w Htw HwWF).
We prove the intermediate claim Hclwsub: closure_of X Tx w ⊆ closure_of X Tx U.
An exact proof term for the current goal is (closure_monotone X Tx w U HTx HwsubU HUsupX).
An exact proof term for the current goal is (Hclwsub z Hzclw2).
We prove the intermediate claim HCeq: closure_of X Tx U = C.
Apply set_ext to the current goal.
An exact proof term for the current goal is HclUsubC.
An exact proof term for the current goal is HCsubclU.
We prove the intermediate claim HCclosed: closed_in X Tx C.
rewrite the current goal using HCeq (from right to left).
An exact proof term for the current goal is (closure_is_closed X Tx U HTx HUsupX).
Set V to be the term X ∖ C.
We prove the intermediate claim HVopen: open_in X Tx V.
An exact proof term for the current goal is (open_of_closed_complement X Tx C HCclosed).
We prove the intermediate claim HVTx: V ∈ Tx.
An exact proof term for the current goal is (open_in_elem X Tx V HVopen).
We prove the intermediate claim HUsubC: U ⊆ C.
rewrite the current goal using HCeq (from right to left).
An exact proof term for the current goal is (subset_of_closure X Tx U HTx HUsupX).
We prove the intermediate claim HUdisjV: U ∩ V = Empty.
Apply Empty_Subq_eq to the current goal.
Let z be given.
Assume Hz: z ∈ U ∩ V.
We will prove z ∈ Empty.
We prove the intermediate claim Hzpair: z ∈ U ∧ z ∈ V.
An exact proof term for the current goal is (binintersectE U V z Hz).
We prove the intermediate claim HzU: z ∈ U.
An exact proof term for the current goal is (andEL (z ∈ U) (z ∈ V) Hzpair).
We prove the intermediate claim HzV: z ∈ V.
An exact proof term for the current goal is (andER (z ∈ U) (z ∈ V) Hzpair).
We prove the intermediate claim HzC: z ∈ C.
An exact proof term for the current goal is (HUsubC z HzU).
We prove the intermediate claim HzNotC: z ∉ C.
An exact proof term for the current goal is (setminusE2 X C z HzV).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HzNotC HzC).
We prove the intermediate claim HBsubV: B ⊆ V.
Let b be given.
Assume HbB: b ∈ B.
We will prove b ∈ V.
We prove the intermediate claim HbX: b ∈ X.
An exact proof term for the current goal is (HBsubX b HbB).
Apply setminusI to the current goal.
An exact proof term for the current goal is HbX.
Assume HbC: b ∈ C.
Apply (UnionE_impred ClWF b HbC) to the current goal.
Let clw be given.
Assume Hbclw: b ∈ clw.
Assume Hclw: clw ∈ ClWF.
Apply (ReplE_impred WF (λw : set ⇒ closure_of X Tx w) clw Hclw False) to the current goal.
Let w be given.
Assume HwWF: w ∈ WF.
Assume Hclweq: clw = closure_of X Tx w.
We prove the intermediate claim Hbclw2: b ∈ closure_of X Tx w.
rewrite the current goal using Hclweq (from right to left).
An exact proof term for the current goal is Hbclw.
We prove the intermediate claim HwW: w ∈ W.
An exact proof term for the current goal is (HWFsubW w HwWF).
We prove the intermediate claim Hexu: ∃u : set, u ∈ Cover ∧ w ⊆ u.
An exact proof term for the current goal is (HWref w HwW).
Apply Hexu to the current goal.
Let u be given.
Assume Hu: u ∈ Cover ∧ w ⊆ u.
We prove the intermediate claim HuCover: u ∈ Cover.
An exact proof term for the current goal is (andEL (u ∈ Cover) (w ⊆ u) Hu).
We prove the intermediate claim Hwsubu: w ⊆ u.
An exact proof term for the current goal is (andER (u ∈ Cover) (w ⊆ u) Hu).
Apply (binunionE {U0} UFam u HuCover) to the current goal.
Assume Hu0: u ∈ {U0}.
We prove the intermediate claim Hueq: u = U0.
An exact proof term for the current goal is (SingE U0 u Hu0).
We prove the intermediate claim HwsubU0: w ⊆ U0.
Let t be given.
Assume Htw: t ∈ w.
We will prove t ∈ U0.
rewrite the current goal using Hueq (from right to left).
An exact proof term for the current goal is (Hwsubu t Htw).
We prove the intermediate claim HwAnon: w ∩ A ≠ Empty.
An exact proof term for the current goal is (SepE2 W (λw0 : set ⇒ w0 ∩ A ≠ Empty) w HwWF).
We prove the intermediate claim HwAsubEmpty: w ∩ A ⊆ Empty.
Let t be given.
Assume Ht: t ∈ w ∩ A.
We will prove t ∈ Empty.
We prove the intermediate claim Htpair: t ∈ w ∧ t ∈ A.
An exact proof term for the current goal is (binintersectE w A t Ht).
We prove the intermediate claim Htw: t ∈ w.
An exact proof term for the current goal is (andEL (t ∈ w) (t ∈ A) Htpair).
We prove the intermediate claim HtA: t ∈ A.
An exact proof term for the current goal is (andER (t ∈ w) (t ∈ A) Htpair).
We prove the intermediate claim HtU0: t ∈ U0.
An exact proof term for the current goal is (HwsubU0 t Htw).
We prove the intermediate claim HtNotA: t ∉ A.
An exact proof term for the current goal is (setminusE2 X A t HtU0).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HtNotA HtA).
We prove the intermediate claim HwAEmpty: w ∩ A = Empty.
An exact proof term for the current goal is (Empty_Subq_eq (w ∩ A) HwAsubEmpty).
Apply FalseE to the current goal.
An exact proof term for the current goal is (HwAnon HwAEmpty).
Assume HuU: u ∈ UFam.
Apply (ReplE_impred A (λa0 : set ⇒ sepU a0) u HuU False) to the current goal.
Let a be given.
Assume HaA: a ∈ A.
Assume Hueq: u = sepU a.
We prove the intermediate claim HwsubSepU: w ⊆ sepU a.
Let t be given.
Assume Htw: t ∈ w.
We will prove t ∈ sepU a.
rewrite the current goal using Hueq (from right to left).
An exact proof term for the current goal is (Hwsubu t Htw).
We prove the intermediate claim Hsep: (sepU a) ∈ Tx ∧ (sepV a) ∈ Tx ∧ a ∈ (sepU a) ∧ B ⊆ (sepV a) ∧ (sepU a) ∩ (sepV a) = Empty.
An exact proof term for the current goal is (HsepProp a HaA).
We prove the intermediate claim Hpqrs: (((sepU a) ∈ Tx ∧ (sepV a) ∈ Tx) ∧ a ∈ (sepU a)) ∧ B ⊆ (sepV a).
An exact proof term for the current goal is (andEL ((((sepU a) ∈ Tx ∧ (sepV a) ∈ Tx) ∧ a ∈ (sepU a)) ∧ B ⊆ (sepV a)) ((sepU a) ∩ (sepV a) = Empty) Hsep).
We prove the intermediate claim HdisjU: (sepU a) ∩ (sepV a) = Empty.
An exact proof term for the current goal is (andER ((((sepU a) ∈ Tx ∧ (sepV a) ∈ Tx) ∧ a ∈ (sepU a)) ∧ B ⊆ (sepV a)) ((sepU a) ∩ (sepV a) = Empty) Hsep).
We prove the intermediate claim HBsubSepV: B ⊆ sepV a.
An exact proof term for the current goal is (andER (((sepU a) ∈ Tx ∧ (sepV a) ∈ Tx) ∧ a ∈ (sepU a)) (B ⊆ (sepV a)) Hpqrs).
We prove the intermediate claim HsepUinTx: sepU a ∈ Tx.
We prove the intermediate claim Hpqr: ((sepU a) ∈ Tx ∧ (sepV a) ∈ Tx) ∧ a ∈ (sepU a).
An exact proof term for the current goal is (andEL (((sepU a) ∈ Tx ∧ (sepV a) ∈ Tx) ∧ a ∈ (sepU a)) (B ⊆ (sepV a)) Hpqrs).
We prove the intermediate claim Hpq: (sepU a) ∈ Tx ∧ (sepV a) ∈ Tx.
An exact proof term for the current goal is (andEL ((sepU a) ∈ Tx ∧ (sepV a) ∈ Tx) (a ∈ (sepU a)) Hpqr).
An exact proof term for the current goal is (andEL ((sepU a) ∈ Tx) ((sepV a) ∈ Tx) Hpq).
We prove the intermediate claim HsepVinTx: sepV a ∈ Tx.
We prove the intermediate claim Hpqr: ((sepU a) ∈ Tx ∧ (sepV a) ∈ Tx) ∧ a ∈ (sepU a).
An exact proof term for the current goal is (andEL (((sepU a) ∈ Tx ∧ (sepV a) ∈ Tx) ∧ a ∈ (sepU a)) (B ⊆ (sepV a)) Hpqrs).
We prove the intermediate claim Hpq: (sepU a) ∈ Tx ∧ (sepV a) ∈ Tx.
An exact proof term for the current goal is (andEL ((sepU a) ∈ Tx ∧ (sepV a) ∈ Tx) (a ∈ (sepU a)) Hpqr).
An exact proof term for the current goal is (andER ((sepU a) ∈ Tx) ((sepV a) ∈ Tx) Hpq).
We prove the intermediate claim HsepUsubX: sepU a ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx (sepU a) HTx HsepUinTx).
We prove the intermediate claim HsepVsubX: sepV a ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx (sepV a) HTx HsepVinTx).
We prove the intermediate claim HsepUsubComp: sepU a ⊆ X ∖ (sepV a).
Let t be given.
Assume HtU: t ∈ sepU a.
We will prove t ∈ X ∖ (sepV a).
We prove the intermediate claim HtX: t ∈ X.
An exact proof term for the current goal is (HsepUsubX t HtU).
Apply setminusI to the current goal.
An exact proof term for the current goal is HtX.
Assume HtV: t ∈ sepV a.
We will prove False.
We prove the intermediate claim HtUV: t ∈ (sepU a) ∩ (sepV a).
An exact proof term for the current goal is (binintersectI (sepU a) (sepV a) t HtU HtV).
We prove the intermediate claim HtEmpty: t ∈ Empty.
rewrite the current goal using HdisjU (from right to left).
An exact proof term for the current goal is HtUV.
An exact proof term for the current goal is ((EmptyE t) HtEmpty).
We prove the intermediate claim HcompClosed: closed_in X Tx (X ∖ (sepV a)).
An exact proof term for the current goal is (closed_of_open_complement X Tx (sepV a) HTx HsepVinTx).
We prove the intermediate claim HclSepUsub: closure_of X Tx (sepU a) ⊆ X ∖ (sepV a).
An exact proof term for the current goal is (closure_subset_of_closed_superset X Tx (sepU a) (X ∖ (sepV a)) HTx HsepUsubComp HcompClosed).
We prove the intermediate claim HclwsubclSepU: closure_of X Tx w ⊆ closure_of X Tx (sepU a).
An exact proof term for the current goal is (closure_monotone X Tx w (sepU a) HTx HwsubSepU HsepUsubX).
We prove the intermediate claim HbNotSepV: b ∉ sepV a.
Assume HbV: b ∈ sepV a.
We will prove False.
We prove the intermediate claim HbclSepU: b ∈ closure_of X Tx (sepU a).
An exact proof term for the current goal is (HclwsubclSepU b Hbclw2).
We prove the intermediate claim HbComp: b ∈ X ∖ (sepV a).
An exact proof term for the current goal is (HclSepUsub b HbclSepU).
We prove the intermediate claim HbNotV: b ∉ sepV a.
An exact proof term for the current goal is (setminusE2 X (sepV a) b HbComp).
An exact proof term for the current goal is (HbNotV HbV).
We prove the intermediate claim HbSepV: b ∈ sepV a.
An exact proof term for the current goal is (HBsubSepV b HbB).
An exact proof term for the current goal is (HbNotSepV HbSepV).
We use U to witness the existential quantifier.
We use V to witness the existential quantifier.
Apply and5I to the current goal.
An exact proof term for the current goal is HUTx.
An exact proof term for the current goal is HVTx.
An exact proof term for the current goal is HAsubU.
An exact proof term for the current goal is HBsubV.
An exact proof term for the current goal is HUdisjV.
∎