let r be real number ; :: 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 in NAT by ORDINAL1:def 13;
assume ( r = k or r = - k ) ; :: thesis: r is Integer
then r in INT by A1, Def1;
hence r is Integer ; :: thesis: verum