let i be Integer; :: thesis: i is finite
i in (NAT \/ [:{0 },NAT :]) \ {[0 ,0 ]} by INT_1:def 2, NUMBERS:def 4;
then ( i in NAT or i in [:{0 },NAT :] ) by XBOOLE_0:def 3;
then ( i in NAT or ex x, y being set st
( x in {0 } & y in NAT & i = [x,y] ) ) by ZFMISC_1:def 2;
hence i is finite ; :: thesis: verum