for V being RealNormSpace
for V1 being SubRealNormSpace of V
for CV1 being Subset of V st V1 is complete & CV1 = the carrier of V1 holds
CV1 is closed