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 ; :: thesis: 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 :: thesis: not m1 >= m2
assume m1 >= m2 ; :: thesis: contradiction
then 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; :: thesis: verum
end;
now :: thesis: not m1 <= m2
assume m1 <= m2 ; :: thesis: contradiction
then 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; :: 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 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 ; :: thesis: verum