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:

consider w being Element of C;
assume A1: C <> {} ; :: thesis:
then reconsider w = w 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 by Def9;
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;
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:
dist w,x <= r by A7, A8;
then A10: dist x,w <= r by A4, METRIC_1:3;
dist w,y <= r by A7, A9;
then A11: (dist x,w) + (dist w,y) <= r + r by A10, XREAL_1:9;
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;