Metamath Proof Explorer


Theorem shssii

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 shssi.1
|- H e. SH
Assertion shssii
|- H C_ ~H

Proof

Step Hyp Ref Expression
1 shssi.1
 |-  H e. SH
2 shss
 |-  ( H e. SH -> H C_ ~H )
3 1 2 ax-mp
 |-  H C_ ~H