ex k being Element of NAT st
( i0 = k or i0 = - k ) by Th2;
hence - i0 is integer by Th1; :: thesis: verum