Metamath Proof Explorer


Theorem shssii

Description: A closed subspace of a Hilbert space is a subset of Hilbert space. (Contributed by NM, 6-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypothesis shssi.1 𝐻S
Assertion shssii 𝐻 ⊆ ℋ

Proof

Step Hyp Ref Expression
1 shssi.1 𝐻S
2 shss ( 𝐻S𝐻 ⊆ ℋ )
3 1 2 ax-mp 𝐻 ⊆ ℋ