theorem :: C0SP3:17

for X being NormedLinearTopSpace holds X is LinearTopSpace ;