let r be Real; :: thesis: ( r is Integer implies ex k being Nat st
( r = k or r = - k ) )
assume r is Integer ; :: thesis: ex k being Nat st
( r = k or r = - k )
then r is Element of INT by Def2;
hence ex k being Nat st
( r = k or r = - k ) by Def1; :: thesis: verum