let r be Real; :: thesis: for k being Nat st ( r = k or r = - k ) holds
r is Integer
let k be Nat; :: thesis: ( ( r = k or r = - k ) implies r is Integer )
assume A1: ( r = k or r = - k ) ; :: thesis: r is Integer
r in INT by A1, Def1;
hence r is Integer ; :: thesis: verum