let n be number ; :: thesis: ( n is integer implies n is real )
assume n is integer ; :: thesis: n is real
then n is Element of INT by Def2;
then reconsider n = n as Element of REAL by Lm3;
n is real ;
hence n is real ; :: thesis: verum