Metamath Proof Explorer

Theorem chel

Description: A member of a closed subspace of a Hilbert space is a vector. (Contributed by NM, 15-Dec-2004) (New usage is discouraged.)

Ref Expression
Assertion chel H C A H A


Step Hyp Ref Expression
1 chss H C H
2 1 sselda H C A H A