let r1, r2 be Real; ( ( 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 ( not C <> {} & r1 = 0 & r2 = 0 implies r1 = r2 )
assume
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 )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 ) )
;
r1 = r2then
(
r1 <= r2 &
r2 <= r1 )
;
hence
r1 = r2
by XXREAL_0:1;
verum
end;
thus
( not C <> {} & r1 = 0 & r2 = 0 implies r1 = r2 )
; verum