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 H C H


Step Hyp Ref Expression
1 chsh H C H S
2 shss H S H
3 1 2 syl H C H