theorem Th8: :: METRIC_6:8

for X being non empty MetrSpace
for S being sequence of X holds
( S is bounded iff ex r being Real ex x being Element of X st
( 0 < r & ( for n being Nat holds S . n in Ball (x,r) ) ) )