theorem Th57: :: CARDFIL4:67

for M being non empty MetrSpace
for p being Point of M
for x being Point of (TopSpaceMetr M)
for s being Function of [:NAT,NAT:],(TopSpaceMetr M) st x = p holds
( x in lim_filter (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) iff for m being non zero Nat ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
s . (n1,n2) in { q where q is Point of M : dist (p,q) < 1 / m } )