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_{1} being Real st b_{1} = 0 )_{1} being Real st b_{1} = 0 )
; :: thesis: verum

( ( 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

proof

thus
( not C <> {} implies ex b
set c = the Element of C;

defpred S_{1}[ 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_{1}[r] } ;

defpred S_{2}[ 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_{2}[r] } ;

A2: for a, b being Real st a in { r where r is Element of REAL : S_{2}[r] } & b in { r where r is Element of REAL : S_{1}[r] } holds

a <= b_{2}[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_{2}[r] }
by A4;

reconsider J = { r where r is Element of REAL : S_{2}[r] } as Subset of REAL by A3;

A6: { r where r is Element of REAL : S_{1}[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_{1}[r] }
by A7;

reconsider I = { r where r is Element of REAL : S_{1}[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

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;defpred S

dist (x,y) <= $1;

set I = { r where r is Element of REAL : S

defpred S

( x in C & y in C & $1 = dist (x,y) );

set J = { r where r is Element of REAL : S

A2: for a, b being Real st a in { r where r is Element of REAL : S

a <= b

proof

A3:
{ r where r is Element of REAL : S
let a, b be Real; :: thesis: ( a in { r where r is Element of REAL : S_{2}[r] } & b in { r where r is Element of REAL : S_{1}[r] } implies a <= b )

assume ( a in { r where r is Element of REAL : S_{2}[r] } & b in { r where r is Element of REAL : S_{1}[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;assume ( a in { r where r is Element of REAL : S

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

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

reconsider J = { r where r is Element of REAL : S

A6: { r where r is Element of REAL : S

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

reconsider I = { r where r is Element of REAL : S

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 s be Real; :: thesis: ( ( for x, y being Point of N st x in C & y in C holds
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;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

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