theorem Th22: :: CARDFIL2:49

for n being natural number holds NAT \ { t where t is Element of NAT : n <= t } is finite