:: deftheorem defines bounded METRIC_6:def 4 :
for X being non empty MetrStruct
for S being sequence of X holds
( S is bounded iff ex r being Real ex x being Element of X st
( 0 < r & rng S c= Ball (x,r) ) );