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

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