for x, y being Point of X st ( for r being Real st r > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist (seq . n),x < r ) & ( for r being Real st r > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist (seq . n),y < r ) holds
x = y
proof
given x,
y being
Point of
X such that A2:
for
r being
Real st
r > 0 holds
ex
m being
Element of
NAT st
for
n being
Element of
NAT st
n >= m holds
dist (seq . n),
x < r
and A3:
for
r being
Real st
r > 0 holds
ex
m being
Element of
NAT st
for
n being
Element of
NAT st
n >= m holds
dist (seq . n),
y < r
and A4:
x <> y
;
:: thesis: contradiction
A5:
dist x,
y > 0
by A4, CSSPACE:57;
then A6:
(dist x,y) / 4
> 0 / 4
by XREAL_1:76;
then consider m1 being
Element of
NAT such that A7:
for
n being
Element of
NAT st
n >= m1 holds
dist (seq . n),
x < (dist x,y) / 4
by A2;
consider m2 being
Element of
NAT such that A8:
for
n being
Element of
NAT st
n >= m2 holds
dist (seq . n),
y < (dist x,y) / 4
by A3, A6;
A9:
now assume
m1 <= m2
;
:: thesis: contradictionthen A10:
dist (seq . m2),
x < (dist x,y) / 4
by A7;
dist (seq . m2),
y < (dist x,y) / 4
by A8;
then A11:
(dist (seq . m2),x) + (dist (seq . m2),y) < ((dist x,y) / 4) + ((dist x,y) / 4)
by A10, XREAL_1:10;
dist x,
y = dist (x - (seq . m2)),
(y - (seq . m2))
by CSSPACE:61;
then
dist x,
y <= (dist (seq . m2),x) + (dist (seq . m2),y)
by CSSPACE:62;
then
dist x,
y <= (dist x,y) / 2
by A11, XXREAL_0:2;
hence
contradiction
by A5, XREAL_1:218;
:: thesis: verum end;
now assume
m1 >= m2
;
:: thesis: contradictionthen A12:
dist (seq . m1),
y < (dist x,y) / 4
by A8;
dist (seq . m1),
x < (dist x,y) / 4
by A7;
then A13:
(dist (seq . m1),x) + (dist (seq . m1),y) < ((dist x,y) / 4) + ((dist x,y) / 4)
by A12, XREAL_1:10;
dist x,
y = dist (x - (seq . m1)),
(y - (seq . m1))
by CSSPACE:61;
then
dist x,
y <= (dist (seq . m1),x) + (dist (seq . m1),y)
by CSSPACE:62;
then
dist x,
y <= (dist x,y) / 2
by A13, XXREAL_0:2;
hence
contradiction
by A5, XREAL_1:218;
:: thesis: verum end;
hence
contradiction
by A9;
:: thesis: verum
end;
hence
for b1, b2 being Point of X st ( for r being Real st r > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist (seq . n),b1 < r ) & ( for r being Real st r > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
dist (seq . n),b2 < r ) holds
b1 = b2
; :: thesis: verum