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

assume A2: 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 ) )
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] } ;
consider r being Real such that
0 < r and
A3: for x, y being Point of N st x in C & y in C holds
dist x,y <= r by A1, Def9;
A4: r in { r where r is Real : S₁[r] } by A3;
consider c being Element of C;
reconsider c = c as Point of N by A2, TARSKI:def 3;
dist c,c = 0 by METRIC_1:1;
then A5: 0 in { r where r is Real : S₂[r] } by A2;
A6: 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 that
A7: a in { r where r is Real : S₂[r] } and
A8: b in { r where r is Real : S₁[r] } ; :: thesis: a <= b
consider t being Real such that
A9: t = a and
A10: ex x, y being Point of N st
( x in C & y in C & t = dist x,y ) by A7;
ex t' being Real st
( t' = b & ( for x, y being Point of N st x in C & y in C holds
dist x,y <= t' ) ) by A8;
hence a <= b by A9, A10; :: thesis: verum

end;

{ r where r is Real : S₁[r] } is Subset of REAL from DOMAIN_1:sch 7();
then reconsider I = { r where r is Real : S₁[r] } as Subset of REAL ;
{ r where r is Real : S₂[r] } is Subset of REAL from DOMAIN_1:sch 7();
then reconsider J = { r where r is Real : S₂[r] } as Subset of REAL ;
consider d being real number such that
A11: for a being real number st a in J holds
a <= d and
A12: for b being real number st b in I holds
d <= b by A4, A5, A6, 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 A11; :: 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 A12; :: thesis: verum

end;

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