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 & ( for x, y being Point of N holds dist x,y <= r ) ) by Def8;
( 0 < r & ( for x, y being Point of N st x in [#] N & y in [#] N holds
dist x,y <= r ) ) by A1;
hence [#] N is bounded by Def9; :: thesis: verum

end;

assume [#] N is bounded ; :: thesis: N is bounded
then consider r being Real such that
A2: ( 0 < r & ( for x, y being Point of N st x in [#] N & y in [#] N holds
dist x,y <= r ) ) by Def9;
take r ; :: according to TBSP_1:def 8 :: thesis: ( 0 < r & ( for x, y being Point of N holds dist x,y <= r ) )
thus 0 < r by A2; :: 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 A2; :: thesis: verum