consider k being Element of NAT such that
A1: ( i1 = k or i1 = - k ) by Th8;
consider l being Element of NAT such that
A2: ( i2 = l or i2 = - l ) by Th8;

A4: now

assume A5: ( i1 = k & i2 = - l ) ; :: thesis: i1 + i2 is Integer

A6: now

assume k - l <= 0 ; :: thesis: k - l is Integer
then k <= 0 + l by XREAL_1:22;
then consider z being Nat such that
A7: l = k + z by NAT_1:10;
- z = (- l) + k by A7;
hence k - l is Integer by Th7; :: thesis: verum

end;

now

assume 0 <= k - l ; :: thesis: k - l is Integer
then 0 + l <= k by XREAL_1:21;
then consider z being Nat such that
A8: k = l + z by NAT_1:10;
thus k - l is Integer by A8; :: thesis: verum

end;

hence i1 + i2 is Integer by A5, A6; :: thesis: verum

end;

A9: now

assume A10: ( i1 = - k & i2 = l ) ; :: thesis: i1 + i2 is Integer

A11: now

assume l - k <= 0 ; :: thesis: l - k is Integer
then l <= 0 + k by XREAL_1:22;
then consider z being Nat such that
A12: k = l + z by NAT_1:10;
- z = (- k) + l by A12;
hence l - k is Integer by Th7; :: thesis: verum

end;

now

assume 0 <= l - k ; :: thesis: l - k is Integer
then 0 + k <= l by XREAL_1:21;
then consider z being Nat such that
A13: l = k + z by NAT_1:10;
thus l - k is Integer by A13; :: thesis: verum

end;

hence i1 + i2 is Integer by A10, A11; :: thesis: verum

end;

now

assume ( i1 = - k & i2 = - l ) ; :: thesis: i1 + i2 is Integer
then i1 + i2 = - (k + l) ;
hence i1 + i2 is Integer by Th7; :: thesis: verum

end;

hence i1 + i2 is integer by A1, A2, A4, A9; :: thesis: verum