let i0 be Integer; :: thesis: ( 0 <= i0 implies i0 in NAT )
assume A1: 0 <= i0 ; :: thesis: i0 in NAT
consider k being Element of NAT such that
A2: ( i0 = k or i0 = - k ) by Th8;
( i0 = - k implies i0 is Element of NAT ) by A1;
hence i0 in NAT by A2; :: thesis: verum