theorem :: CARDFIL4:68

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)
for s2 being Function of [:NAT,NAT:],M st x = p & s = s2 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
s2 . (n1,n2) in { q where q is Point of M : dist (p,q) < 1 / m } ) by Th57;