let T be non empty TopStruct ; :: thesis: for s being sequence of T

for x being Point of T holds

( x in Lim s iff for U1 being Subset of T st U1 is open & x in U1 holds

ex n being Nat st

for m being Nat st n <= m holds

s . m in U1 )

let s be sequence of T; :: thesis: for x being Point of T holds

( x in Lim s iff for U1 being Subset of T st U1 is open & x in U1 holds

ex n being Nat st

for m being Nat st n <= m holds

s . m in U1 )

let x be Point of T; :: thesis: ( x in Lim s iff for U1 being Subset of T st U1 is open & x in U1 holds

ex n being Nat st

for m being Nat st n <= m holds

s . m in U1 )

( x in Lim s iff s is_convergent_to x ) by FRECHET:def 5;

hence ( x in Lim s iff for U1 being Subset of T st U1 is open & x in U1 holds

ex n being Nat st

for m being Nat st n <= m holds

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

for x being Point of T holds

( x in Lim s iff for U1 being Subset of T st U1 is open & x in U1 holds

ex n being Nat st

for m being Nat st n <= m holds

s . m in U1 )

let s be sequence of T; :: thesis: for x being Point of T holds

( x in Lim s iff for U1 being Subset of T st U1 is open & x in U1 holds

ex n being Nat st

for m being Nat st n <= m holds

s . m in U1 )

let x be Point of T; :: thesis: ( x in Lim s iff for U1 being Subset of T st U1 is open & x in U1 holds

ex n being Nat st

for m being Nat st n <= m holds

s . m in U1 )

( x in Lim s iff s is_convergent_to x ) by FRECHET:def 5;

hence ( x in Lim s iff for U1 being Subset of T st U1 is open & x in U1 holds

ex n being Nat st

for m being Nat st n <= m holds

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