for x, y being Point of X st ( for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
dist ((seq . n),x) < r ) & ( for r being Real st r > 0 holds
ex m being Nat st
for n being 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
Nat st
for
n being
Nat st
n >= m holds
dist (
(seq . n),
x)
< r
and A3:
for
r being
Real st
r > 0 holds
ex
m being
Nat st
for
n being
Nat st
n >= m holds
dist (
(seq . n),
y)
< r
and A4:
x <> y
;
contradiction
A5:
dist (
x,
y)
> 0
by A4, BHSP_1:38;
then A6:
(dist (x,y)) / 4
> 0 / 4
by XREAL_1:74;
then consider m1 being
Nat such that A7:
for
n being
Nat st
n >= m1 holds
dist (
(seq . n),
x)
< (dist (x,y)) / 4
by A2;
consider m2 being
Nat such that A8:
for
n being
Nat st
n >= m2 holds
dist (
(seq . n),
y)
< (dist (x,y)) / 4
by A3, A6;
A9:
now not m1 >= m2assume
m1 >= m2
;
contradictionthen A10:
dist (
(seq . m1),
y)
< (dist (x,y)) / 4
by A8;
dist (
x,
y)
= dist (
(x - (seq . m1)),
(y - (seq . m1)))
by BHSP_1:42;
then A11:
dist (
x,
y)
<= (dist ((seq . m1),x)) + (dist ((seq . m1),y))
by BHSP_1:43;
dist (
(seq . m1),
x)
< (dist (x,y)) / 4
by A7;
then
(dist ((seq . m1),x)) + (dist ((seq . m1),y)) < ((dist (x,y)) / 4) + ((dist (x,y)) / 4)
by A10, XREAL_1:8;
then
dist (
x,
y)
<= (dist (x,y)) / 2
by A11, XXREAL_0:2;
hence
contradiction
by A5, XREAL_1:216;
verum end;
now not m1 <= m2assume
m1 <= m2
;
contradictionthen A12:
dist (
(seq . m2),
x)
< (dist (x,y)) / 4
by A7;
dist (
x,
y)
= dist (
(x - (seq . m2)),
(y - (seq . m2)))
by BHSP_1:42;
then A13:
dist (
x,
y)
<= (dist ((seq . m2),x)) + (dist ((seq . m2),y))
by BHSP_1:43;
dist (
(seq . m2),
y)
< (dist (x,y)) / 4
by A8;
then
(dist ((seq . m2),x)) + (dist ((seq . m2),y)) < ((dist (x,y)) / 4) + ((dist (x,y)) / 4)
by A12, XREAL_1:8;
then
dist (
x,
y)
<= (dist (x,y)) / 2
by A13, XXREAL_0:2;
hence
contradiction
by A5, XREAL_1:216;
verum end;
hence
contradiction
by A9;
verum
end;
hence
for b1, b2 being Point of X st ( for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
dist ((seq . n),b1) < r ) & ( for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
dist ((seq . n),b2) < r ) holds
b1 = b2
; verum