theorem :: REAL_NS2:69

for V being RealLinearSpace
for F being set holds
( F is Subset of V iff F is Subset of (RLSp2RVSp V) ) ;