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 )

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

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
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;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

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