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 )

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

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

assume A4:
N is symmetric
; :: thesis: ( not N is triangle or for r being Real
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 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

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

hence
C is bounded
; :: thesis: verum
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 A10, XREAL_1:7;

dist (x,y) <= (dist (x,w)) + (dist (w,y)) by A5, METRIC_1:4;

hence dist (x,y) <= r + r by A11, XXREAL_0:2; :: thesis: verum

end;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 A10, XREAL_1:7;

dist (x,y) <= (dist (x,w)) + (dist (w,y)) by A5, METRIC_1:4;

hence dist (x,y) <= r + r by A11, XXREAL_0:2; :: thesis: verum