let x be Element of [:base_of_frechet_filter,base_of_frechet_filter:]; :: thesis: ex n being Nat st square-uparrow n c= x
ex i, j being Nat st x = [:(NAT \ (Segm i)),(NAT \ (Segm j)):] by Th31;
hence ex n being Nat st square-uparrow n c= x by Th28; :: thesis: verum