let p be Rational; :: thesis: ( 1 < denominator p iff not p is integer )

now

assume A1: p is not Integer ; :: thesis: denominator p > 1
denominator p >= 1 by Th29;
hence denominator p > 1 by A1, Th41, XXREAL_0:1; :: thesis: verum

end;

hence ( 1 < denominator p iff not p is integer ) by Th40; :: thesis: verum