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_{1}, b_{2} 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),b_{1}) < 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),b_{2}) < r ) holds

b_{1} = b_{2}
; :: thesis: verum

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

hence
for b
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;

end;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;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

now :: thesis: not m1 <= m2

hence
contradiction
by A9; :: thesis: verumassume
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;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

ex m being Nat st

for n being Nat st n >= m holds

dist ((seq . n),b

ex m being Nat st

for n being Nat st n >= m holds

dist ((seq . n),b

b