let M be non empty MetrSpace; :: thesis: for p being Point of M
for x being Point of ()
for s being Function of ,() st x = p holds
( x in lim_filter (s,) 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 } )

let p be Point of M; :: thesis: for x being Point of ()
for s being Function of ,() st x = p holds
( x in lim_filter (s,) 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 } )

let x be Point of (); :: thesis: for s being Function of ,() st x = p holds
( x in lim_filter (s,) 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 } )

let s be Function of ,(); :: thesis: ( x = p implies ( x in lim_filter (s,) 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 } ) )

assume A1: x = p ; :: thesis: ( x in lim_filter (s,) 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 } )

( x in lim_filter (s,) 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 } )
proof
hereby :: thesis: ( ( 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 } ) implies x in lim_filter (s,) )
assume A2: x in lim_filter (s,) ; :: thesis: 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 }

hereby :: thesis: verum
let m be non zero Nat; :: thesis: 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 }

set B = { q where q is Point of M : dist (p,q) < 1 / m } ;
A3: { q where q is Point of M : dist (p,q) < 1 / m } = Ball (p,(1 / m)) by METRIC_1:def 14;
ex y being Point of M st
( y = x & Balls x = { (Ball (y,(1 / m))) where m is Nat : m <> 0 } ) by FRECHET:def 1;
then A4: { q where q is Point of M : dist (p,q) < 1 / m } in Balls x by A3, A1;
Balls x is basis of () by CARDFIL3:6;
hence 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 } by A2, A4, Th54; :: thesis: verum
end;
end;
assume A5: 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 } ; :: thesis:
A6: Balls x is basis of () by CARDFIL3:6;
for B being Element of Balls x ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
s . (n1,n2) in B
proof
let B be Element of Balls x; :: thesis: ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
s . (n1,n2) in B

consider y being Point of M such that
A7: y = x and
A8: Balls x = { (Ball (y,(1 / m))) where m is Nat : m <> 0 } by FRECHET:def 1;
B in Balls x ;
then consider m0 being Nat such that
A9: B = Ball (y,(1 / m0)) and
A10: m0 <> 0 by A8;
consider n0 being Nat such that
A11: for n1, n2 being Nat st n0 <= n1 & n0 <= n2 holds
s . (n1,n2) in { q where q is Point of M : dist (p,q) < 1 / m0 } by ;
for n1, n2 being Nat st n0 <= n1 & n0 <= n2 holds
s . (n1,n2) in B
proof
let n1, n2 be Nat; :: thesis: ( n0 <= n1 & n0 <= n2 implies s . (n1,n2) in B )
assume ( n0 <= n1 & n0 <= n2 ) ; :: thesis: s . (n1,n2) in B
then s . (n1,n2) in { q where q is Point of M : dist (p,q) < 1 / m0 } by A11;
hence s . (n1,n2) in B by ; :: thesis: verum
end;
hence ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
s . (n1,n2) in B ; :: thesis: verum
end;
hence x in lim_filter (s,) by ; :: thesis: verum
end;
hence ( x in lim_filter (s,) 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 } ) ; :: thesis: verum