for x being set st x in INT holds
x in INT- \/ NAT

proof

let x be set ; :: thesis: ( x in INT implies x in INT- \/ NAT )
assume x in INT ; :: thesis: x in INT- \/ NAT
then consider k being Element of NAT such that
A1: ( x = k or x = - k ) by INT_1:def 1;

now

per cases ( x = k or x = - k ) by A1;

suppose x = k ; :: thesis: x in INT- \/ NAT

hence x in INT- \/ NAT by XBOOLE_0:def 3; :: thesis: verum

end;

suppose x = - k ; :: thesis: x in INT- \/ NAT

then x in INT- by Def1;
hence x in INT- \/ NAT by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence x in INT- \/ NAT ; :: thesis: verum

end;

then A2: INT c= INT- \/ NAT by TARSKI:def 3;
for x being set st x in INT- \/ NAT holds
x in INT

proof

let x be set ; :: thesis: ( x in INT- \/ NAT implies x in INT )
assume A3: x in INT- \/ NAT ; :: thesis: x in INT

now

per cases ( x in INT- or x in NAT ) by A3, XBOOLE_0:def 3;

suppose x in INT- ; :: thesis: x in INT

then ex k being Element of NAT st x = - k by Def1;
hence x in INT by INT_1:def 1; :: thesis: verum

end;

suppose x in NAT ; :: thesis: x in INT

hence x in INT by INT_1:def 1; :: thesis: verum

end;

end;

end;

hence x in INT ; :: thesis: verum

end;

then INT- \/ NAT c= INT by TARSKI:def 3;
hence INT = INT- \/ NAT by A2, XBOOLE_0:def 10; :: thesis: verum