let N be non empty MetrStruct ; :: thesis: ( N is bounded iff [#] N is bounded )
thus ( N is bounded implies [#] N is bounded ) :: thesis: ( [#] N is bounded implies N is bounded )

proof

assume N is bounded ; :: thesis: [#] N is bounded
then consider r being Real such that
A1: 0 < r and
A2: for x, y being Point of N holds dist (x,y) <= r ;
for x, y being Point of N st x in [#] N & y in [#] N holds
dist (x,y) <= r by A2;
hence [#] N is bounded by A1; :: thesis: verum

end;

assume [#] N is bounded ; :: thesis: N is bounded
then consider r being Real such that
A3: 0 < r and
A4: for x, y being Point of N st x in [#] N & y in [#] N holds
dist (x,y) <= r ;
take r ; :: according to TBSP_1:def 6 :: thesis: ( 0 < r & ( for x, y being Point of N holds dist (x,y) <= r ) )
thus 0 < r by A3; :: thesis: for x, y being Point of N holds dist (x,y) <= r
let x, y be Point of N; :: thesis: dist (x,y) <= r
thus dist (x,y) <= r by A4; :: thesis: verum