:: deftheorem defines bounded TBSP_1:def 6 :
for N being non empty MetrStruct holds
( N is bounded iff ex r being Real st
( 0 < r & ( for x, y being Point of N holds dist (x,y) <= r ) ) );