let X be non empty MetrSpace; :: thesis:
let x be Element of X; :: thesis:
let S be sequence of X; :: thesis:
assume A1: S is_convergent_in_metrspace_to x ; :: thesis:
thus for r being Real st 0 < r holds
Ball (x,r) contains_almost_all_sequence S :: thesis:

proof

let r be Real; :: thesis:
assume A2: 0 < r ; :: thesis:
ex m being Nat st
for n being Nat st m <= n holds
S . n in Ball (x,r)

proof

consider m1 being Nat such that
A3: for n being Nat st m1 <= n holds
dist ((S . n),x) < r by A1, A2;
take k = m1; :: thesis:

now :: thesis:

let n be Nat; :: thesis:
assume k <= n ; :: thesis:
then dist (x,(S . n)) < r by A3;
hence S . n in Ball (x,r) by METRIC_1:11; :: thesis:

end;

hence for n being Nat st k <= n holds
S . n in Ball (x,r) ; :: thesis:

end;

hence Ball (x,r) contains_almost_all_sequence S ; :: thesis:

end;