for X being RealNormSpace
for Y being RealBanachSpace
for X0 being Subset of Y st X is Subspace of Y & the carrier of X = X0 & the normF of X = the normF of Y | the carrier of X & X0 is closed holds
X is complete