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 A1: M is bounded ; :: thesis: for X being Subset of M holds X is bounded
let X be Subset of M; :: thesis: X is bounded
[#] M is bounded by A1;
hence X is bounded by TBSP_1:14; :: 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:18; :: thesis: verum