let x be object ; :: thesis: ( x is integer implies x is rational )
assume x is integer ; :: thesis: x is rational
then reconsider x = x as Integer ;
x = x / 1 ;
hence x is rational by Th3; :: thesis: verum