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

proof

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

proof

assume A2: x in I ; :: thesis: ex k being Nat st
( x = k or x = - k )
then A3: not x in {[0,0]} by A1, NUMBERS:def 4, XBOOLE_0:def 5;

per cases ( x in NAT or x in [:{0},NAT:] ) by A1, A2, NUMBERS:def 4, XBOOLE_0:def 3;

suppose x in NAT ; :: thesis: ex k being Nat st
( x = k or x = - k )

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

end;

suppose x in [:{0},NAT:] ; :: thesis: ex k being Nat st
( x = k or x = - k )

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: verum

end;

end;

end;

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

per cases ( x = k or ( x = - k & k <> x ) ) by A4;

suppose x = k ; :: thesis: x in I

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: verum

end;

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

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: verum

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: I = INT
thus I c= INT :: according to XBOOLE_0:def 10 :: thesis: INT c= I

proof

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

per cases ( x = k or ( x = - k & k <> x ) ) by A10;

suppose x = k ; :: thesis: x in INT

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: verum

end;

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

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: verum

end;

end;

end;

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

per cases ( x in NAT or x in [:{0},NAT:] ) by A15, NUMBERS:def 4, XBOOLE_0:def 3;

suppose x in NAT ; :: thesis: x in I

hence x in I by A9; :: thesis: verum

end;

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

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: verum

end;

end;