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 b₁ being Real st b₁ = 0 )

proof

set c = the Element of C;
defpred S₁[ 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 : S₁[r] } ;
defpred S₂[ 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 : S₂[r] } ;
A2: for a, b being Real st a in { r where r is Element of REAL : S₂[r] } & b in { r where r is Element of REAL : S₁[r] } holds
a <= b

proof

let a, b be Real; :: thesis: ( a in { r where r is Element of REAL : S₂[r] } & b in { r where r is Element of REAL : S₁[r] } implies a <= b )
assume ( a in { r where r is Element of REAL : S₂[r] } & b in { r where r is Element of REAL : S₁[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 : S₂[r] } is Subset of REAL from DOMAIN_1:sch 7();
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 : S₂[r] } by A4;
reconsider J = { r where r is Element of REAL : S₂[r] } as Subset of REAL by A3;
A6: { r where r is Element of REAL : S₁[r] } is Subset of REAL from DOMAIN_1:sch 7();
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 : S₁[r] } by A7;
reconsider I = { r where r is Element of REAL : S₁[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 A8, A5, A2, MEMBERED:37;
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 b₁ being Real st b₁ = 0 ) ; :: thesis: verum