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