theorem :: CARDFIL4:37

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