Metamath Proof Explorer

Theorem cheli

Description: A member of a closed subspace of a Hilbert space is a vector. (Contributed by NM, 6-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypothesis chssi.1 H C
Assertion cheli A H A


Step Hyp Ref Expression
1 chssi.1 H C
2 1 chssii H
3 2 sseli A H A