for T being non empty TopStruct
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 )