let M be non empty MetrStruct ; :: thesis: ( M is bounded iff for X being Subset of M holds X is bounded )

hereby :: thesis: ( ( for X being Subset of M holds X is bounded ) implies M is bounded )

assume M is bounded ; :: thesis: for X being Subset of M holds X is bounded
then A1: [#] M is bounded by TBSP_1:25;
let X be Subset of M; :: thesis: X is bounded
thus X is bounded by A1, TBSP_1:21; :: thesis: verum

end;

assume for X being Subset of M holds X is bounded ; :: thesis: M is bounded
then [#] M is bounded ;
hence M is bounded by TBSP_1:25; :: thesis: verum