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 )
hereby :: thesis: ( ex n being Nat st square-uparrow n c= s " M implies 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;
given n being Nat such that A2: square-uparrow n c= s " M ; :: thesis: s " M in <.(Frechet_Filter NAT),(Frechet_Filter NAT).)
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