let p be Rational; :: thesis: ( p is Integer implies ( denominator p = 1 & numerator p = p ) )
assume p is Integer ; :: thesis: ( denominator p = 1 & numerator p = p )
then reconsider m = p as Integer ;
p = m / 1 ;
then A1: denominator p <= 1 by Def3;
1 <= denominator p by Th8;
hence denominator p = 1 by A1, XXREAL_0:1; :: thesis: numerator p = p
hence numerator p = p ; :: thesis: verum