theorem Th6: :: CARDFIL3:9

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_f s iff for b being Element of Balls x ex i being Nat st
for j being Nat st i <= j holds
s . j in b )