Metamath Proof Explorer


Theorem chss

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

Ref Expression
Assertion chss ( 𝐻C𝐻 ⊆ ℋ )

Proof

Step Hyp Ref Expression
1 chsh ( 𝐻C𝐻S )
2 shss ( 𝐻S𝐻 ⊆ ℋ )
3 1 2 syl ( 𝐻C𝐻 ⊆ ℋ )