A1: 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 A2: x in INT ; :: thesis: x in INT- \/ NAT
consider k being Element of NAT such that
A3: ( x = k or x = - k ) by A2, INT_1:def 1;

A4: now

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

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

thus x in INT- \/ NAT by A5, XBOOLE_0:def 3; :: thesis: verum

end;

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

A7: x in INT- by A6, Def1;
thus x in INT- \/ NAT by A7, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

thus x in INT- \/ NAT by A4; :: thesis: verum

end;

A8: INT c= INT- \/ NAT by A1, TARSKI:def 3;
A9: 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 A10: x in INT- \/ NAT ; :: thesis: x in INT

A11: now

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

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

A13: ex k being Element of NAT st x = - k by A12, Def1;
thus x in INT by A13, INT_1:def 1; :: thesis: verum

end;

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

thus x in INT by A14, INT_1:def 1; :: thesis: verum

end;

end;

end;

thus x in INT by A11; :: thesis: verum

end;

A15: INT- \/ NAT c= INT by A9, TARSKI:def 3;
thus INT = INT- \/ NAT by A8, A15, XBOOLE_0:def 10; :: thesis: verum