theorem :: CARDFIL4:36

for A being finite Subset of [:NAT,NAT:] ex n being Nat st A c= square-downarrow n