thus ( C <> {} implies ex r being Real st
( ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= r ) & ( for s being Real st ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= s ) holds
r <= s ) ) ) :: thesis: ( not C <> {} implies ex b1 being Real st b1 = 0 )
proof
set c = the Element of C;
defpred S1[ Real] means for x, y being Point of N st x in C & y in C holds
dist (x,y) <= \$1;
set I = { r where r is Element of REAL : S1[r] } ;
defpred S2[ set ] means ex x, y being Point of N st
( x in C & y in C & \$1 = dist (x,y) );
set J = { r where r is Element of REAL : S2[r] } ;
A2: for a, b being Real st a in { r where r is Element of REAL : S2[r] } & b in { r where r is Element of REAL : S1[r] } holds
a <= b
proof
let a, b be Real; :: thesis: ( a in { r where r is Element of REAL : S2[r] } & b in { r where r is Element of REAL : S1[r] } implies a <= b )
assume ( a in { r where r is Element of REAL : S2[r] } & b in { r where r is Element of REAL : S1[r] } ) ; :: thesis: a <= b
then ( ex t being Element of REAL st
( t = a & ex x, y being Point of N st
( x in C & y in C & t = dist (x,y) ) ) & ex t9 being Element of REAL st
( t9 = b & ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= t9 ) ) ) ;
hence a <= b ; :: thesis: verum
end;
A3: { r where r is Element of REAL : S2[r] } is Subset of REAL from assume A4: C <> {} ; :: thesis: ex r being Real st
( ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= r ) & ( for s being Real st ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= s ) holds
r <= s ) )

then reconsider c = the Element of C as Point of N by TARSKI:def 3;
dist (c,c) = 0 by METRIC_1:1;
then A5: In (0,REAL) in { r where r is Element of REAL : S2[r] } by A4;
reconsider J = { r where r is Element of REAL : S2[r] } as Subset of REAL by A3;
A6: { r where r is Element of REAL : S1[r] } is Subset of REAL from consider r being Real such that
0 < r and
A7: for x, y being Point of N st x in C & y in C holds
dist (x,y) <= r by A1;
reconsider r = r as Element of REAL by XREAL_0:def 1;
A8: r in { r where r is Element of REAL : S1[r] } by A7;
reconsider I = { r where r is Element of REAL : S1[r] } as Subset of REAL by A6;
consider d being Real such that
A9: for a being Real st a in J holds
a <= d and
A10: for b being Real st b in I holds
d <= b by ;
take d ; :: thesis: ( ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= d ) & ( for s being Real st ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= s ) holds
d <= s ) )

thus for x, y being Point of N st x in C & y in C holds
dist (x,y) <= d :: thesis: for s being Real st ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= s ) holds
d <= s
proof
let x, y be Point of N; :: thesis: ( x in C & y in C implies dist (x,y) <= d )
assume A11: ( x in C & y in C ) ; :: thesis: dist (x,y) <= d
dist (x,y) in REAL by XREAL_0:def 1;
then dist (x,y) in J by A11;
hence dist (x,y) <= d by A9; :: thesis: verum
end;
let s be Real; :: thesis: ( ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= s ) implies d <= s )

assume A12: for x, y being Point of N st x in C & y in C holds
dist (x,y) <= s ; :: thesis: d <= s
reconsider s = s as Element of REAL by XREAL_0:def 1;
s in I by A12;
hence d <= s by A10; :: thesis: verum
end;
thus ( not C <> {} implies ex b1 being Real st b1 = 0 ) ; :: thesis: verum