for T being non empty TopSpace
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 )