for x being Element of [:base_of_frechet_filter,base_of_frechet_filter:] ex n being Nat st square-uparrow n c= x