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