theorem Th6: :: REAL_NS3:6

for Nrm being RealNormSpace
for X being Subset of Nrm st X is compact holds
( X is closed & ex r being Real st
for y being Point of Nrm st y in X holds
||.y.|| < r )