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

consider c being 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 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 Real : S₂[r] } ;
A2: for a, b being real number st a in { r where r is Real : S₂[r] } & b in { r where r is Real : S₁[r] } holds
a <= b

proof

let a, b be real number ; :: thesis: ( a in { r where r is Real : S₂[r] } & b in { r where r is Real : S₁[r] } implies a <= b )
assume ( a in { r where r is Real : S₂[r] } & b in { r where r is Real : S₁[r] } ) ; :: thesis: a <= b
then ( ex t being 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 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 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 = c as Point of N by TARSKI:def 3;
dist c,c = 0 by METRIC_1:1;
then A5: 0 in { r where r is Real : S₂[r] } by A4;
reconsider J = { r where r is Real : S₂[r] } as Subset of REAL by A3;
A6: { r where r is 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, Def9;
A8: r in { r where r is Real : S₁[r] } by A7;
reconsider I = { r where r is Real : S₁[r] } as Subset of REAL by A6;
consider d being real number such that
A9: for a being real number st a in J holds
a <= d and
A10: for b being real number st b in I holds
d <= b by A8, A5, A2, MEMBERED:37;
take d ; :: thesis: ( d is Real & ( 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 d is Real by XREAL_0:def 1; :: 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 ( x in C & y in C ) ; :: thesis: dist x,y <= d
then dist x,y in J ;
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 for x, y being Point of N st x in C & y in C holds
dist x,y <= s ; :: thesis: d <= s
then s in I ;
hence d <= s by A10; :: thesis: verum

end;

thus ( not C <> {} implies ex b₁ being Real st b₁ = 0 ) ; :: thesis: verum