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 )

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 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).))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

end;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;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

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

hence
x in lim_filter (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).))
by Th48; :: thesis: verumlet 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;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