let p be Rational; :: thesis: ( 1 > (denominator p) " iff not p is integer )
A1: (denominator p) " <= 1 by Th34;

now

assume p is not Integer ; :: thesis: (denominator p) " < 1
then (denominator p) " <> 1 by Lm7, Th41;
hence (denominator p) " < 1 by A1, XXREAL_0:1; :: thesis: verum

end;

hence ( 1 > (denominator p) " iff not p is integer ) by Lm7, Th40; :: thesis: verum