[:{0},NAT:] is countable by CARD_4:7;
then NAT \/ [:{0},NAT:] is countable by CARD_2:85;
hence INT is denumerable by NUMBERS:def 4; :: thesis: verum