theorem :: TOPREAL6:64

for M being non empty MetrStruct holds
( M is bounded iff for X being Subset of M holds X is bounded )