let T be non empty TopSpace; :: thesis: 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 s .: (square-uparrow n) c= B )
let s be Function of [:NAT,NAT:], the carrier of T; :: thesis: 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 s .: (square-uparrow n) c= B )
let x be Point of T; :: thesis: 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 s .: (square-uparrow n) c= B )
let cB be basis of (BOOL2F (NeighborhoodSystem x)); :: thesis: ( x in lim_filter (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) iff for B being Element of cB ex n being Nat st s .: (square-uparrow n) c= B )

hereby :: thesis: ( ( for B being Element of cB ex n being Nat st s .: (square-uparrow n) c= B ) implies x in lim_filter (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) )

assume A1: x in lim_filter (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) ; :: thesis: for B being Element of cB ex n being Nat st s .: (square-uparrow n) c= B

hereby :: thesis: verum

let B be Element of cB; :: thesis: ex n being Nat st s .: (square-uparrow n) c= B
consider n being Nat such that
A2: square-uparrow n c= s " B by A1, Th48;
take n = n; :: thesis: s .: (square-uparrow n) c= B
A3: s .: (square-uparrow n) c= s .: (s " B) by A2, RELAT_1:123;
s .: (s " B) c= B by FUNCT_1:75;
hence s .: (square-uparrow n) c= B by A3; :: thesis: verum

end;

end;

assume A4: for B being Element of cB ex n being Nat st s .: (square-uparrow n) c= B ; :: thesis: x in lim_filter (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).))

now :: thesis: for B being Element of cB ex n being Nat st square-uparrow n c= s " B

let B be Element of cB; :: thesis: ex n being Nat st square-uparrow n c= s " B
consider n being Nat such that
A5: s .: (square-uparrow n) c= B by A4;
A6: s " (s .: (square-uparrow n)) c= s " B by A5, RELAT_1:143;
dom s = [:NAT,NAT:] by FUNCT_2:def 1;
then square-uparrow n c= s " (s .: (square-uparrow n)) by FUNCT_1:76;
then square-uparrow n c= s " B by A6;
hence ex n being Nat st square-uparrow n c= s " B ; :: thesis: verum

end;

hence x in lim_filter (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).)) by Th48; :: thesis: verum