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