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

proof

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

proof

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

now

let n be Element of NAT ; :: thesis: ( k <= n implies S . n in Ball x,r )
assume k <= n ; :: thesis: S . n in Ball x,r
then dist x,(S . n) < r by A3;
hence S . n in Ball x,r by METRIC_1:12; :: thesis: verum

end;

hence for n being Element of NAT st k <= n holds
S . n in Ball x,r ; :: thesis: verum

end;

hence Ball x,r contains_almost_all_sequence S by Def12; :: thesis: verum

end;