let p be Rational; :: thesis: ( 1 > (denominator p) " iff not p is integer )
A1: (denominator p) " <= 1 by Th10;
now :: thesis: ( p is not Integer implies (denominator p) " < 1 )
assume p is not Integer ; :: thesis: (denominator p) " < 1
then (denominator p) " <> 1 by Lm7, Th15;
hence (denominator p) " < 1 by A1, XXREAL_0:1; :: thesis: verum
end;
hence ( 1 > (denominator p) " iff not p is integer ) by Lm7, Th14; :: thesis: verum