let N be non empty MetrStruct ; :: thesis:
let C be Subset of N; :: thesis:
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:

set w = the Element of C;
assume A1: C <> {} ; :: thesis:
then reconsider w = the Element of C as Point of N by TARSKI:def 3;
assume C is bounded ; :: thesis:
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:
take w ; :: thesis:
thus 0 < r by A2; :: thesis:
thus w in C by A1; :: thesis:
let z be Point of N; :: thesis:
assume z in C ; :: thesis:
hence dist (w,z) <= r by A3; :: thesis:

end;

assume A4: N is symmetric ; :: thesis:
assume A5: N is triangle ; :: thesis:
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:
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 ) )

take r + r ; :: thesis:
thus 0 < r + r by A6; :: thesis:
let x, y be Point of N; :: thesis:
assume that
A8: x in C and
A9: y in C ; :: thesis:
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:

end;