for n being Nat holds square-downarrow n is finite Subset of [:NAT,NAT:]