for N being non empty MetrStruct
for C being Subset of N holds
( ( C <> {} & C is bounded implies ex r being Real ex w being Element of N st
( 0 < r & w in C & ( for z being Point of N st z in C holds
dist (w,z) <= r ) ) ) & ( N is symmetric & N is triangle & ex r being Real ex w being Element of N st
( 0 < r & ( for z being Point of N st z in C holds
dist (w,z) <= r ) ) implies C is bounded ) )