Let X, Tx, U and x be given.
Assume Hreg: regular_space X Tx.
Assume HU: U ∈ Tx.
Assume HxU: x ∈ U.
We will prove ∃V : set, V ∈ Tx ∧ x ∈ V ∧ closure_of X Tx V ⊆ U.
We prove the intermediate claim HTx: topology_on X Tx.
An exact proof term for the current goal is (regular_space_topology_on X Tx Hreg).
We prove the intermediate claim HTsub: Tx ⊆ 𝒫 X.
An exact proof term for the current goal is (topology_subset_axiom X Tx HTx).
We prove the intermediate claim HUPow: U ∈ 𝒫 X.
An exact proof term for the current goal is (HTsub U HU).
We prove the intermediate claim HUsX: U ⊆ X.
An exact proof term for the current goal is (PowerE X U HUPow).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HUsX x HxU).
Set F to be the term X ∖ U.
We prove the intermediate claim HFcl: closed_in X Tx F.
An exact proof term for the current goal is (closed_of_open_complement X Tx U HTx HU).
We prove the intermediate claim HxnotF: x ∉ F.
Assume HxF: x ∈ F.
We prove the intermediate claim HxNotU: x ∉ U.
An exact proof term for the current goal is (setminusE2 X U x HxF).
An exact proof term for the current goal is (HxNotU HxU).
We prove the intermediate claim Hsep: ∃U0 V0 : set, U0 ∈ Tx ∧ V0 ∈ Tx ∧ x ∈ U0 ∧ F ⊆ V0 ∧ U0 ∩ V0 = Empty.
An exact proof term for the current goal is (andER (one_point_sets_closed X Tx) (∀x0 : set, x0 ∈ X → ∀F0 : set, closed_in X Tx F0 → x0 ∉ F0 → ∃U0 V0 : set, U0 ∈ Tx ∧ V0 ∈ Tx ∧ x0 ∈ U0 ∧ F0 ⊆ V0 ∧ U0 ∩ V0 = Empty) Hreg x HxX F HFcl HxnotF).
Apply Hsep to the current goal.
Let U0 be given.
Assume HexV0: ∃V0 : set, U0 ∈ Tx ∧ V0 ∈ Tx ∧ x ∈ U0 ∧ F ⊆ V0 ∧ U0 ∩ V0 = Empty.
Apply HexV0 to the current goal.
Let V0 be given.
Assume Hpack: U0 ∈ Tx ∧ V0 ∈ Tx ∧ x ∈ U0 ∧ F ⊆ V0 ∧ U0 ∩ V0 = Empty.
We prove the intermediate claim Habcd: ((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ x ∈ U0) ∧ F ⊆ V0.
An exact proof term for the current goal is (andEL (((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ x ∈ U0) ∧ F ⊆ V0) (U0 ∩ V0 = Empty) Hpack).
We prove the intermediate claim Hdisj: U0 ∩ V0 = Empty.
An exact proof term for the current goal is (andER (((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ x ∈ U0) ∧ F ⊆ V0) (U0 ∩ V0 = Empty) Hpack).
We prove the intermediate claim Habc: (U0 ∈ Tx ∧ V0 ∈ Tx) ∧ x ∈ U0.
An exact proof term for the current goal is (andEL ((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ x ∈ U0) (F ⊆ V0) Habcd).
We prove the intermediate claim HFV0: F ⊆ V0.
An exact proof term for the current goal is (andER ((U0 ∈ Tx ∧ V0 ∈ Tx) ∧ x ∈ U0) (F ⊆ V0) Habcd).
We prove the intermediate claim H12: U0 ∈ Tx ∧ V0 ∈ Tx.
An exact proof term for the current goal is (andEL (U0 ∈ Tx ∧ V0 ∈ Tx) (x ∈ U0) Habc).
We prove the intermediate claim HxU0: x ∈ U0.
An exact proof term for the current goal is (andER (U0 ∈ Tx ∧ V0 ∈ Tx) (x ∈ U0) Habc).
We prove the intermediate claim HU0Tx: U0 ∈ Tx.
An exact proof term for the current goal is (andEL (U0 ∈ Tx) (V0 ∈ Tx) H12).
We prove the intermediate claim HV0Tx: V0 ∈ Tx.
An exact proof term for the current goal is (andER (U0 ∈ Tx) (V0 ∈ Tx) H12).
We prove the intermediate claim HU0sub: U0 ⊆ X.
We prove the intermediate claim HU0Pow: U0 ∈ 𝒫 X.
An exact proof term for the current goal is (HTsub U0 HU0Tx).
An exact proof term for the current goal is (PowerE X U0 HU0Pow).
We prove the intermediate claim HU0subC: U0 ⊆ X ∖ V0.
Let y be given.
Assume HyU0: y ∈ U0.
We will prove y ∈ X ∖ V0.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (HU0sub y HyU0).
We prove the intermediate claim HyNotV0: y ∉ V0.
Assume HyV0: y ∈ V0.
We prove the intermediate claim HyInt: y ∈ U0 ∩ V0.
An exact proof term for the current goal is (binintersectI U0 V0 y HyU0 HyV0).
We prove the intermediate claim HyE: y ∈ Empty.
rewrite the current goal using Hdisj (from right to left).
An exact proof term for the current goal is HyInt.
An exact proof term for the current goal is (EmptyE y HyE).
An exact proof term for the current goal is (setminusI X V0 y HyX HyNotV0).
We prove the intermediate claim HCcl: closed_in X Tx (X ∖ V0).
An exact proof term for the current goal is (closed_of_open_complement X Tx V0 HTx HV0Tx).
We prove the intermediate claim HclU0subC: closure_of X Tx U0 ⊆ (X ∖ V0).
An exact proof term for the current goal is (closure_subset_of_closed_superset X Tx U0 (X ∖ V0) HTx HU0subC HCcl).
We prove the intermediate claim HCsubU: (X ∖ V0) ⊆ U.
Let y be given.
Assume HyC: y ∈ (X ∖ V0).
We will prove y ∈ U.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (setminusE1 X V0 y HyC).
We prove the intermediate claim HyNotV0: y ∉ V0.
An exact proof term for the current goal is (setminusE2 X V0 y HyC).
We prove the intermediate claim HyNotF: y ∉ F.
Assume HyF: y ∈ F.
We prove the intermediate claim HyV0: y ∈ V0.
An exact proof term for the current goal is (HFV0 y HyF).
An exact proof term for the current goal is (HyNotV0 HyV0).
We prove the intermediate claim HyUF: y ∈ X ∖ F.
An exact proof term for the current goal is (setminusI X F y HyX HyNotF).
We prove the intermediate claim HXFeq: X ∖ F = U.
We prove the intermediate claim HFdef: F = X ∖ U.
Use reflexivity.
rewrite the current goal using HFdef (from left to right) at position 1.
An exact proof term for the current goal is (setminus_setminus_eq X U HUsX).
rewrite the current goal using HXFeq (from right to left).
An exact proof term for the current goal is HyUF.
We use U0 to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HU0Tx.
An exact proof term for the current goal is HxU0.
An exact proof term for the current goal is (Subq_tra (closure_of X Tx U0) (X ∖ V0) U HclU0subC HCsubU).
∎