theorem Th8: :: CARDFIL3:11

for M being non empty MetrSpace
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 )