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 that A13:
for
x,
y being
Point of
N st
x in C &
y in C holds
dist x,
y <= r1
and A14:
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
and A15:
for
x,
y being
Point of
N st
x in C &
y in C holds
dist x,
y <= r2
and A16:
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 = r2A17:
r1 <= r2
by A14, A15;
r2 <= r1
by A13, A16;
hence
r1 = r2
by A17, XXREAL_0:1;
:: thesis: verum
end;
thus
( not C <> {} & r1 = 0 & r2 = 0 implies r1 = r2 )
; :: thesis: verum