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 square-uparrow n c= s " 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 square-uparrow n c= s " 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 square-uparrow n c= s " 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 square-uparrow n c= s " 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 square-uparrow n c= s " 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 square-uparrow n c= s " 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 square-uparrow n c= s " 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 square-uparrow n c= s " B )

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

assume A2:
for B being Element of cB ex n being Nat st square-uparrow n c= s " 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 square-uparrow n c= s " B

end;hereby :: thesis: verum

let B be Element of cB; :: thesis: ex n being Nat st square-uparrow n c= s " B

B is a_neighborhood of x by YELLOW19:2;

hence ex n being Nat st square-uparrow n c= s " B by A1, Th47; :: thesis: verum

end;B is a_neighborhood of x by YELLOW19:2;

hence ex n being Nat st square-uparrow n c= s " B by A1, Th47; :: thesis: verum

now :: thesis: for A being a_neighborhood of x ex n being Nat st square-uparrow n c= s " A

hence
x in lim_filter (s,<.(Frechet_Filter NAT),(Frechet_Filter NAT).))
by Th47; :: thesis: verumlet A be a_neighborhood of x; :: thesis: ex n being Nat st square-uparrow n c= s " A

A3: A is Element of BOOL2F (NeighborhoodSystem x) by YELLOW19:2;

cB is filter_basis ;

then consider B being Element of cB such that

A4: B c= A by A3;

A5: ex n being Nat st square-uparrow n c= s " B by A2;

s " B c= s " A by A4, RELAT_1:145;

hence ex n being Nat st square-uparrow n c= s " A by A5, XBOOLE_1:1; :: thesis: verum

end;A3: A is Element of BOOL2F (NeighborhoodSystem x) by YELLOW19:2;

cB is filter_basis ;

then consider B being Element of cB such that

A4: B c= A by A3;

A5: ex n being Nat st square-uparrow n c= s " B by A2;

s " B c= s " A by A4, RELAT_1:145;

hence ex n being Nat st square-uparrow n c= s " A by A5, XBOOLE_1:1; :: thesis: verum