theorem :: C0SP3:18

for X being NormedLinearTopSpace holds X is RealNormSpace ;