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

proof

let x be object ; :: thesis: ( x in INT implies x in INT- \/ NAT )
assume x in INT ; :: thesis: x in INT- \/ NAT
then consider k being Nat such that
A1: ( x = k or x = - k ) by INT_1:def 1;
A2: k in NAT by ORDINAL1:def 12;

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, A2; :: thesis: verum

end;

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

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

end;

end;

end;

then A3: INT c= INT- \/ NAT ;
for x being object st x in INT- \/ NAT holds
x in INT

proof

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

now :: thesis: x in INT

per cases ( x in INT- or x in NAT ) by A4, 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 ;
hence INT = INT- \/ NAT by A3, XBOOLE_0:def 10; :: thesis: verum