theorem :: CARDFIL4:28

for n being Nat holds square-uparrow n is infinite Subset of [:NAT,NAT:]