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

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

assume 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;

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