let I be set ; :: thesis:
thus ( I = INT implies for x being object holds
( x in I iff ex k being Nat st
( x = k or x = - k ) ) ) :: thesis:

proof

assume A1: I = INT ; :: thesis:
let x be object ; :: thesis:
thus ( x in I implies ex k being Nat st
( x = k or x = - k ) ) :: thesis:

proof

assume A2: x in I ; :: thesis:
then A3: not x in {[0,0]} by A1, NUMBERS:def 4, XBOOLE_0:def 5;

per cases by A1, A2, NUMBERS:def 4, XBOOLE_0:def 3;

suppose x in NAT ; :: thesis:

hence ex k being Nat st
( x = k or x = - k ) ; :: thesis:

end;

suppose x in [:{0},NAT:] ; :: thesis:

then x in [:{0},NAT:] \ {[0,0]} by A3, XBOOLE_0:def 5;
hence ex k being Nat st
( x = k or x = - k ) by Lm1; :: thesis:

end;

end;

end;

given k being Nat such that A4: ( x = k or x = - k ) ; :: thesis:

per cases by A4;

suppose x = k ; :: thesis:

then A5: x in NAT by ORDINAL1:def 12;
then x in REAL by NUMBERS:19;
then A6: not x in {[0,0]} by NUMBERS:def 1, XBOOLE_0:def 5;
x in NAT \/ [:{0},NAT:] by XBOOLE_0:def 3, A5;
hence x in I by A1, A6, NUMBERS:def 4, XBOOLE_0:def 5; :: thesis:

end;

suppose ( x = - k & k <> x ) ; :: thesis:

then A7: x in [:{0},NAT:] \ {[0,0]} by Lm2;
then A8: not x in {[0,0]} by XBOOLE_0:def 5;
x in NAT \/ [:{0},NAT:] by A7, XBOOLE_0:def 3;
hence x in I by A1, A8, NUMBERS:def 4, XBOOLE_0:def 5; :: thesis:

end;

end;

end;

assume A9: for x being object holds
( x in I iff ex k being Nat st
( x = k or x = - k ) ) ; :: thesis:
thus I c= INT :: according to XBOOLE_0:def 10 :: thesis:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in I ; :: thesis:
then consider k being Nat such that
A10: ( x = k or x = - k ) by A9;

per cases by A10;

suppose x = k ; :: thesis:

then A11: x in NAT by ORDINAL1:def 12;
then x in REAL by NUMBERS:19;
then A12: not x in {[0,0]} by NUMBERS:def 1, XBOOLE_0:def 5;
x in NAT \/ [:{0},NAT:] by XBOOLE_0:def 3, A11;
hence x in INT by A12, NUMBERS:def 4, XBOOLE_0:def 5; :: thesis:

end;

suppose ( x = - k & k <> x ) ; :: thesis:

then A13: x in [:{0},NAT:] \ {[0,0]} by Lm2;
then A14: not x in {[0,0]} by XBOOLE_0:def 5;
x in NAT \/ [:{0},NAT:] by A13, XBOOLE_0:def 3;
hence x in INT by A14, NUMBERS:def 4, XBOOLE_0:def 5; :: thesis:

end;

end;

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A15: x in INT ; :: thesis:
then A16: not x in {[0,0]} by NUMBERS:def 4, XBOOLE_0:def 5;

per cases by A15, NUMBERS:def 4, XBOOLE_0:def 3;

suppose x in NAT ; :: thesis:

hence x in I by A9; :: thesis:

end;

suppose x in [:{0},NAT:] ; :: thesis:

then x in [:{0},NAT:] \ {[0,0]} by A16, XBOOLE_0:def 5;
then ex k being Nat st
( x = k or x = - k ) by Lm1;
hence x in I by A9; :: thesis:

end;

end;