theorem :: REAL_NS3:38

for V being finite-dimensional RealNormSpace
for X being Subset of V st dim V <> 0 holds
( X is compact iff ( X is closed & ex r being Real st
for y being Point of V st y in X holds
||.y.|| < r ) )