:: deftheorem defines totally_bounded TBSP_1:def 1 :
for N being non empty MetrStruct holds
( N is totally_bounded iff for r being Real st r > 0 holds
ex G being Subset-Family of N st
( G is finite & the carrier of N = union G & ( for C being Subset of N st C in G holds
ex w being Element of N st C = Ball (w,r) ) ) );