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