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 )