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:

assume A1: C <> {} ; :: thesis:
assume C is bounded ; :: thesis:
then consider r being Real such that
A2: ( 0 < r & ( for x, y being Point of N st x in C & y in C holds
dist x,y <= r ) ) by Def9;
take r ; :: thesis:
consider w being Element of C;
reconsider w = w as Point of N by A1, TARSKI:def 3;
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 A2; :: thesis:

end;

assume A3: N is symmetric ; :: thesis:
assume A4: N is triangle ; :: thesis:
given r being Real, w being Element of N such that A5: ( 0 < r & w in C & ( 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 A5; :: thesis:
let x, y be Point of N; :: thesis:
assume ( x in C & y in C ) ; :: thesis:
then ( dist w,x <= r & dist w,y <= r ) by A5;
then ( dist x,w <= r & dist w,y <= r ) by A3, METRIC_1:3;
then A7: (dist x,w) + (dist w,y) <= r + r by XREAL_1:9;
dist x,y <= (dist x,w) + (dist w,y) by A4, METRIC_1:4;
hence dist x,y <= r + r by A7, XXREAL_0:2; :: thesis:

end;

hence C is bounded by Def9; :: thesis: