let M be non empty MetrSpace; :: thesis: for s being sequence of the carrier of (TopSpaceMetr M)
for x being Point of (TopSpaceMetr M) holds
( 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 )
let s be sequence of the carrier of (TopSpaceMetr M); :: thesis: for x being Point of (TopSpaceMetr M) holds
( 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 )
let x be Point of (TopSpaceMetr M); :: thesis: ( 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 )

now :: thesis: ( ( x in Lim s & 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 ) & ( ( for b being Element of Balls x ex n being Nat st
for m being Nat st n <= m holds
s . m in b ) implies x in Lim s ) )

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

assume A1: x in Lim s ; :: thesis: ( 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 )

now :: thesis: for b being Element of Balls x ex n0 being Nat st
for m being Nat st n0 <= m holds
s . m in b

let b be Element of Balls x; :: thesis: ex n0 being Nat st
for m being Nat st n0 <= m holds
s . m in b
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: for m being Nat st n0 <= m holds
s . m in b
thus for m being Nat st n0 <= m holds
s . m in b by A3, A5; :: thesis: verum

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: verum

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: x in Lim s

now :: thesis: for U1 being Subset of (TopSpaceMetr M) st U1 is open & x in U1 holds
ex n0 being Nat st
for m being Nat st n0 <= m holds
s . m in U1

let U1 be Subset of (TopSpaceMetr M); :: thesis: ( U1 is open & x in U1 implies ex n0 being Nat st
for m being Nat st n0 <= m holds
s . m in U1 )
assume ( U1 is open & x in U1 ) ; :: thesis: ex n0 being Nat st
for m being Nat st n0 <= m holds
s . m in U1
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: for m being Nat st n0 <= m holds
s . m in U1
thus for m being Nat st n0 <= m holds
s . m in U1 by A9, A8; :: thesis: verum

end;

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

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: verum