Let m, V and y be given.
Assume HmO: m ∈ ω.
Assume HVsubE: V ⊆ (euclidean_space m).
Assume HVopenE: open_in (euclidean_space m) (euclidean_topology m) V.
Assume HyV: y ∈ V.
We prove the intermediate claim HregE: regular_space (euclidean_space m) (euclidean_topology m).
An exact proof term for the current goal is (euclidean_space_regular m).
We prove the intermediate claim HVinT: V ∈ (euclidean_topology m).
An exact proof term for the current goal is (open_in_elem (euclidean_space m) (euclidean_topology m) V HVopenE).
An exact proof term for the current goal is (regular_space_open_nbhd_closure_sub (euclidean_space m) (euclidean_topology m) V y HregE HVinT HyV).
∎