let N be non empty MetrStruct ; :: thesis: for C being Subset of N holds
( ( C <> {} & C is bounded implies ex r being Real ex w being Element of N st
( 0 < r & w in C & ( for z being Point of N st z in C holds
dist (w,z) <= r ) ) ) & ( N is symmetric & N is triangle & ex r being Real ex w being Element of N st
( 0 < r & ( for z being Point of N st z in C holds
dist (w,z) <= r ) ) implies C is bounded ) )

let C be Subset of N; :: thesis: ( ( C <> {} & C is bounded implies ex r being Real ex w being Element of N st
( 0 < r & w in C & ( for z being Point of N st z in C holds
dist (w,z) <= r ) ) ) & ( N is symmetric & N is triangle & ex r being Real ex w being Element of N st
( 0 < r & ( for z being Point of N st z in C holds
dist (w,z) <= r ) ) implies C is bounded ) )

thus ( C <> {} & C is bounded implies ex r being Real ex w being Element of N st
( 0 < r & w in C & ( for z being Point of N st z in C holds
dist (w,z) <= r ) ) ) :: thesis: ( N is symmetric & N is triangle & ex r being Real ex w being Element of N st
( 0 < r & ( for z being Point of N st z in C holds
dist (w,z) <= r ) ) implies C is bounded )
proof
set w = the Element of C;
assume A1: C <> {} ; :: thesis: ( not C is bounded or ex r being Real ex w being Element of N st
( 0 < r & w in C & ( for z being Point of N st z in C holds
dist (w,z) <= r ) ) )

then reconsider w = the Element of C as Point of N by TARSKI:def 3;
assume C is bounded ; :: thesis: ex r being Real ex w being Element of N st
( 0 < r & w in C & ( for z being Point of N st z in C holds
dist (w,z) <= r ) )

then consider r being Real such that
A2: 0 < r and
A3: for x, y being Point of N st x in C & y in C holds
dist (x,y) <= r ;
take r ; :: thesis: ex w being Element of N st
( 0 < r & w in C & ( for z being Point of N st z in C holds
dist (w,z) <= r ) )

take w ; :: thesis: ( 0 < r & w in C & ( for z being Point of N st z in C holds
dist (w,z) <= r ) )

thus 0 < r by A2; :: thesis: ( w in C & ( for z being Point of N st z in C holds
dist (w,z) <= r ) )

thus w in C by A1; :: thesis: for z being Point of N st z in C holds
dist (w,z) <= r

let z be Point of N; :: thesis: ( z in C implies dist (w,z) <= r )
assume z in C ; :: thesis: dist (w,z) <= r
hence dist (w,z) <= r by A3; :: thesis: verum
end;
assume A4: N is symmetric ; :: thesis: ( not N is triangle or for r being Real
for w being Element of N holds
( not 0 < r or ex z being Point of N st
( z in C & not dist (w,z) <= r ) ) or C is bounded )

assume A5: N is triangle ; :: thesis: ( for r being Real
for w being Element of N holds
( not 0 < r or ex z being Point of N st
( z in C & not dist (w,z) <= r ) ) or C is bounded )

given r being Real, w being Element of N such that A6: 0 < r and
A7: for z being Point of N st z in C holds
dist (w,z) <= r ; :: thesis: C is bounded
set s = r + r;
reconsider N = N as symmetric MetrStruct by A4;
reconsider w = w as Element of N ;
ex s being Real st
( 0 < s & ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= s ) )
proof
take r + r ; :: thesis: ( 0 < r + r & ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= r + r ) )

thus 0 < r + r by A6; :: thesis: for x, y being Point of N st x in C & y in C holds
dist (x,y) <= r + r

let x, y be Point of N; :: thesis: ( x in C & y in C implies dist (x,y) <= r + r )
assume that
A8: x in C and
A9: y in C ; :: thesis: dist (x,y) <= r + r
A10: dist (w,x) <= r by A7, A8;
dist (w,y) <= r by A7, A9;
then A11: (dist (x,w)) + (dist (w,y)) <= r + r by ;
dist (x,y) <= (dist (x,w)) + (dist (w,y)) by ;
hence dist (x,y) <= r + r by ; :: thesis: verum
end;
hence C is bounded ; :: thesis: verum