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