Let X, Tx, A, B and x be given.
Assume Hreg: regular_space X Tx.
Assume HxX: x ∈ X.
Assume HB: B ∈ Tx.
Assume HxB: x ∈ B.
Assume HAcl: closed_in X Tx A.
Assume HAint: interior_of X Tx A = Empty.
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 HnotSub: ¬ (B ⊆ A).
An exact proof term for the current goal is (point_in_open_empty_interior_not_subset X Tx A B x HTx HAint HB HxB).
We prove the intermediate claim Hexx1: ∃x1 : set, x1 ∈ B ∧ x1 ∉ A.
An exact proof term for the current goal is (not_subset_ex_elem A B HnotSub).
Apply Hexx1 to the current goal.
Let x1 be given.
Assume Hx1pair: x1 ∈ B ∧ x1 ∉ A.
We prove the intermediate claim Hx1B: x1 ∈ B.
An exact proof term for the current goal is (andEL (x1 ∈ B) (x1 ∉ A) Hx1pair).
We prove the intermediate claim Hx1notA: x1 ∉ A.
An exact proof term for the current goal is (andER (x1 ∈ B) (x1 ∉ A) Hx1pair).
We prove the intermediate claim HBsubX: B ⊆ X.
An exact proof term for the current goal is (topology_elem_subset X Tx B HTx HB).
We prove the intermediate claim Hx1X: x1 ∈ X.
An exact proof term for the current goal is (HBsubX x1 Hx1B).
We prove the intermediate claim HopenComp: open_in X Tx (X ∖ A).
An exact proof term for the current goal is (open_of_closed_complement X Tx A HAcl).
We prove the intermediate claim HXATx: (X ∖ A) ∈ Tx.
An exact proof term for the current goal is (open_in_elem X Tx (X ∖ A) HopenComp).
Set W to be the term (B ∩ (X ∖ A)).
We prove the intermediate claim HWTx: W ∈ Tx.
An exact proof term for the current goal is (topology_binintersect_closed X Tx B (X ∖ A) HTx HB HXATx).
We prove the intermediate claim Hx1XA: x1 ∈ (X ∖ A).
An exact proof term for the current goal is (setminusI X A x1 Hx1X Hx1notA).
We prove the intermediate claim Hx1W: x1 ∈ W.
An exact proof term for the current goal is (binintersectI B (X ∖ A) x1 Hx1B Hx1XA).
We prove the intermediate claim HexV: ∃V : set, V ∈ Tx ∧ x1 ∈ V ∧ closure_of X Tx V ⊆ W.
An exact proof term for the current goal is (regular_space_open_nbhd_closure_sub X Tx W x1 Hreg HWTx Hx1W).
Apply HexV to the current goal.
Let V be given.
Assume HVpack: V ∈ Tx ∧ x1 ∈ V ∧ closure_of X Tx V ⊆ W.
We use x1 to witness the existential quantifier.
We use V to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hx1pair.
An exact proof term for the current goal is HVpack.
∎