let T be non empty TopSpace; :: thesis: for s being Function of [:NAT,NAT:], the carrier of T

for M being Subset of the carrier of T holds

( s " M in <.(Frechet_Filter NAT),(Frechet_Filter NAT).) iff ex n being Nat st square-uparrow n c= s " M )

let s be Function of [:NAT,NAT:], the carrier of T; :: thesis: for M being Subset of the carrier of T holds

( s " M in <.(Frechet_Filter NAT),(Frechet_Filter NAT).) iff ex n being Nat st square-uparrow n c= s " M )

let M be Subset of the carrier of T; :: thesis: ( s " M in <.(Frechet_Filter NAT),(Frechet_Filter NAT).) iff ex n being Nat st square-uparrow n c= s " M )

square-uparrow n in { (square-uparrow n) where n is Nat : verum } ;

then ex b2 being Element of [:base_of_frechet_filter,base_of_frechet_filter:] st b2 c= square-uparrow n by Th34;

then A3: ex b2 being Element of [:base_of_frechet_filter,base_of_frechet_filter:] st b2 c= s " M by A2, XBOOLE_1:1;

dom s = [:NAT,NAT:] by FUNCT_2:def 1;

then s " M is Subset of [:NAT,NAT:] by RELAT_1:132;

hence s " M in <.(Frechet_Filter NAT),(Frechet_Filter NAT).) by A3, Th35, CARDFIL2:def 8; :: thesis: verum

for M being Subset of the carrier of T holds

( s " M in <.(Frechet_Filter NAT),(Frechet_Filter NAT).) iff ex n being Nat st square-uparrow n c= s " M )

let s be Function of [:NAT,NAT:], the carrier of T; :: thesis: for M being Subset of the carrier of T holds

( s " M in <.(Frechet_Filter NAT),(Frechet_Filter NAT).) iff ex n being Nat st square-uparrow n c= s " M )

let M be Subset of the carrier of T; :: thesis: ( s " M in <.(Frechet_Filter NAT),(Frechet_Filter NAT).) iff ex n being Nat st square-uparrow n c= s " M )

hereby :: thesis: ( ex n being Nat st square-uparrow n c= s " M implies s " M in <.(Frechet_Filter NAT),(Frechet_Filter NAT).) )

given n being Nat such that A2:
square-uparrow n c= s " M
; :: thesis: s " M in <.(Frechet_Filter NAT),(Frechet_Filter NAT).)assume
s " M in <.(Frechet_Filter NAT),(Frechet_Filter NAT).)
; :: thesis: ex n being Nat st square-uparrow n c= s " M

then consider b being Element of [:base_of_frechet_filter,base_of_frechet_filter:] such that

A1: b c= s " M by Th35, CARDFIL2:def 8;

ex n being Nat st square-uparrow n c= b by Th32;

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

end;then consider b being Element of [:base_of_frechet_filter,base_of_frechet_filter:] such that

A1: b c= s " M by Th35, CARDFIL2:def 8;

ex n being Nat st square-uparrow n c= b by Th32;

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

square-uparrow n in { (square-uparrow n) where n is Nat : verum } ;

then ex b2 being Element of [:base_of_frechet_filter,base_of_frechet_filter:] st b2 c= square-uparrow n by Th34;

then A3: ex b2 being Element of [:base_of_frechet_filter,base_of_frechet_filter:] st b2 c= s " M by A2, XBOOLE_1:1;

dom s = [:NAT,NAT:] by FUNCT_2:def 1;

then s " M is Subset of [:NAT,NAT:] by RELAT_1:132;

hence s " M in <.(Frechet_Filter NAT),(Frechet_Filter NAT).) by A3, Th35, CARDFIL2:def 8; :: thesis: verum