Metamath Proof Explorer


Theorem chssii

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 chssi.1 𝐻C
Assertion chssii 𝐻 ⊆ ℋ

Proof

Step Hyp Ref Expression
1 chssi.1 𝐻C
2 1 chshii 𝐻S
3 2 shssii 𝐻 ⊆ ℋ