Theorem hlphl

Description: Every subcomplex Hilbert space is an inner product space (also called a pre-Hilbert space). (Contributed by NM, 28-Apr-2007) (Revised by Mario Carneiro, 15-Oct-2015)

	Ref	Expression
Assertion	hlphl	|- ( W e. CHil -> W e. PreHil )

Proof

Step	Hyp	Ref	Expression
1		hlcph	|- ( W e. CHil -> W e. CPreHil )
2		cphphl	|- ( W e. CPreHil -> W e. PreHil )
3	1 2	syl	|- ( W e. CHil -> W e. PreHil )