for n being Nat
for X being Subset of (REAL-NS n) holds
( X is compact iff ( X is closed & ex r being Real st
for y being Point of (REAL-NS n) st y in X holds
||.y.|| < r ) ) by Lm3, Th6;