Let X and N be given.
Assume HN: N ∈ ω.
Assume HXsub: X ⊆ (euclidean_space N).
Assume Hcl: closed_in (euclidean_space N) (euclidean_topology N) X.
Set EN to be the term euclidean_space N.
Set TN to be the term euclidean_topology N.
Set TX to be the term subspace_topology EN TN X.
We prove the intermediate claim HdimEN: covering_dimension EN TN N.
An exact proof term for the current goal is (euclidean_space_covering_dimension_le N HN).
An exact proof term for the current goal is (dimension_closed_subspace_le EN TN X N HdimEN Hcl).
∎