let r1, r2 be Real; :: thesis: ( ( C <> {} & ( for x, y being Point of N st x in C & y in C holds

dist (x,y) <= r1 ) & ( 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

r1 <= s ) & ( for x, y being Point of N st x in C & y in C holds

dist (x,y) <= r2 ) & ( 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

r2 <= s ) implies r1 = r2 ) & ( not C <> {} & r1 = 0 & r2 = 0 implies r1 = r2 ) )

dist (x,y) <= r1 ) & ( 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

r1 <= s ) & ( for x, y being Point of N st x in C & y in C holds

dist (x,y) <= r2 ) & ( 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

r2 <= s ) implies r1 = r2 ) & ( not C <> {} & r1 = 0 & r2 = 0 implies r1 = r2 ) )

hereby :: thesis: ( not C <> {} & r1 = 0 & r2 = 0 implies r1 = r2 )

thus
( not C <> {} & r1 = 0 & r2 = 0 implies r1 = r2 )
; :: thesis: verumassume
C <> {}
; :: thesis: ( ( for x, y being Point of N st x in C & y in C holds

dist (x,y) <= r1 ) & ( 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

r1 <= s ) & ( for x, y being Point of N st x in C & y in C holds

dist (x,y) <= r2 ) & ( 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

r2 <= s ) implies r1 = r2 )

assume ( ( for x, y being Point of N st x in C & y in C holds

dist (x,y) <= r1 ) & ( 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

r1 <= s ) & ( for x, y being Point of N st x in C & y in C holds

dist (x,y) <= r2 ) & ( 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

r2 <= s ) ) ; :: thesis: r1 = r2

then ( r1 <= r2 & r2 <= r1 ) ;

hence r1 = r2 by XXREAL_0:1; :: thesis: verum

end;dist (x,y) <= r1 ) & ( 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

r1 <= s ) & ( for x, y being Point of N st x in C & y in C holds

dist (x,y) <= r2 ) & ( 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

r2 <= s ) implies r1 = r2 )

assume ( ( for x, y being Point of N st x in C & y in C holds

dist (x,y) <= r1 ) & ( 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

r1 <= s ) & ( for x, y being Point of N st x in C & y in C holds

dist (x,y) <= r2 ) & ( 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

r2 <= s ) ) ; :: thesis: r1 = r2

then ( r1 <= r2 & r2 <= r1 ) ;

hence r1 = r2 by XXREAL_0:1; :: thesis: verum