let T be non empty TopSpace; for s being Function of [:NAT,NAT:], the carrier of T
for x being Point of T
for cB being basis of (BOOL2F (NeighborhoodSystem x)) holds
( x in lim_filter (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) iff for B being Element of cB ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
s . (n1,n2) in B )
let s be Function of [:NAT,NAT:], the carrier of T; for x being Point of T
for cB being basis of (BOOL2F (NeighborhoodSystem x)) holds
( x in lim_filter (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) iff for B being Element of cB ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
s . (n1,n2) in B )
let x be Point of T; for cB being basis of (BOOL2F (NeighborhoodSystem x)) holds
( x in lim_filter (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) iff for B being Element of cB ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
s . (n1,n2) in B )
let cB be basis of (BOOL2F (NeighborhoodSystem x)); ( x in lim_filter (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) iff for B being Element of cB ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
s . (n1,n2) in B )
( ( for B being Element of cB ex n being Nat st s .: (square-uparrow n) c= B ) iff for B being Element of cB ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
s . (n1,n2) in B )
hence
( x in lim_filter (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) iff for B being Element of cB ex n being Nat st
for n1, n2 being Nat st n <= n1 & n <= n2 holds
s . (n1,n2) in B )
by Th50; verum