let x be Integer; :: thesis: x is Rational
x = x / 1 ;
hence x is Rational by Th6; :: thesis: verum