let i0 be Integer; :: thesis: ( 0 <= i0 implies i0 in NAT )
consider k being Nat such that
A1: ( i0 = k or i0 = - k ) by Th2;
assume 0 <= i0 ; :: thesis: i0 in NAT
then ( i0 = - k implies i0 is Element of NAT ) ;
hence i0 in NAT by A1, ORDINAL1:def 12; :: thesis: verum