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 )

for m being Nat st n <= m holds

s . m in b ) ; :: thesis: verum

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 ) )

for m being Nat st n <= m holds

s . m in b ; :: thesis: x in Lim s

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 ) & ( ( 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 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 ) 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 )

for m being Nat st n <= m holds

s . m in b ) ; :: thesis: verum

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

hence
( x in Lim s implies for b being Element of Balls x ex n 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;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

for m being Nat st n <= m holds

s . m in b ) ; :: thesis: verum

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

hence
x in Lim s
by Th7; :: thesis: verumex 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;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

for m being Nat st n <= m holds

s . m in b ) ; :: thesis: verum