let M be non empty MetrSpace; :: thesis:
let s be sequence of the carrier of (TopSpaceMetr M); :: thesis:
let x be Point of (TopSpaceMetr M); :: thesis:

hereby :: thesis:

assume A1: x in Lim s ; :: thesis:

let b be Element of Balls x; :: thesis:
Balls x is basis of (BOOL2F (NeighborhoodSystem x)) by Th5;
then Balls x c= BOOL2F (NeighborhoodSystem x) ;
then b in BOOL2F (NeighborhoodSystem x) ;
then b in NeighborhoodSystem x by CARDFIL2:def 20;
then b is a_neighborhood of x by YELLOW19:2;
then consider V being Subset of (TopSpaceMetr M) such that
A2: V is open and
A3: V c= b and
A4: x in V by CONNSP_2:6;
consider n0 being Nat such that
A5: for m being Nat st n0 <= m holds
s . m in V by A2, A4, A1, Th7;
take n0 = n0; :: thesis:
thus for m being Nat st n0 <= m holds
s . m in b by A3, A5; :: thesis:

end;

hence ( x in Lim s implies for b being Element of Balls x ex n being Nat st
for m being Nat st n <= m holds
s . m in b ) ; :: thesis:

end;

assume A6: for b being Element of Balls x ex n being Nat st
for m being Nat st n <= m holds
s . m in b ; :: thesis:

let U1 be Subset of (TopSpaceMetr M); :: thesis:
assume ( U1 is open & x in U1 ) ; :: thesis:
then U1 is a_neighborhood of x by CONNSP_2:6;
then U1 in NeighborhoodSystem x by YELLOW19:2;
then A7: U1 is Element of BOOL2F (NeighborhoodSystem x) by CARDFIL2:def 20;
reconsider BAX = Balls x as non empty Subset of (BOOL2F (NeighborhoodSystem x)) by Th5;
BAX is filter_basis by Th5;
then consider b being Element of Balls x such that
A8: b c= U1 by A7;
consider n0 being Nat such that
A9: for m being Nat st n0 <= m holds
s . m in b by A6;
take n0 = n0; :: thesis:
thus for m being Nat st n0 <= m holds
s . m in U1 by A9, A8; :: thesis:

end;

hence x in Lim s by Th7; :: thesis:

end;

hence ( x in Lim s iff for b being Element of Balls x ex n being Nat st
for m being Nat st n <= m holds
s . m in b ) ; :: thesis: