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