Description: A closed subspace is a subset of the base. (Contributed by Mario Carneiro, 13Oct2015)
Ref  Expression  

Hypotheses  cssss.v   V = ( Base ` W ) 

cssss.c   C = ( ClSubSp ` W ) 

Assertion  cssss   ( S e. C > S C_ V ) 
Step  Hyp  Ref  Expression 

1  cssss.v   V = ( Base ` W ) 

2  cssss.c   C = ( ClSubSp ` W ) 

3  eqid   ( ocv ` W ) = ( ocv ` W ) 

4  3 2  cssi   ( S e. C > S = ( ( ocv ` W ) ` ( ( ocv ` W ) ` S ) ) ) 
5  1 3  ocvss   ( ( ocv ` W ) ` ( ( ocv ` W ) ` S ) ) C_ V 
6  4 5  eqsstrdi   ( S e. C > S C_ V ) 