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 
|- CH C_ ~P ~H

Proof

Step Hyp Ref Expression
1 chsssh 
 |-  CH C_ SH
2 shsspwh 
 |-  SH C_ ~P ~H
3 1 2 sstri 
 |-  CH C_ ~P ~H