Metamath Proof Explorer


Theorem chsspwh

Description: Closed subspaces are subsets of Hilbert space. (Contributed by NM, 24-Nov-2004) (New usage is discouraged.)

Ref Expression
Assertion chsspwh C 𝒫

Proof

Step Hyp Ref Expression
1 chsssh C S
2 shsspwh S 𝒫
3 1 2 sstri C 𝒫