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

now :: thesis: ( p is not Integer implies denominator p > 1 )

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

end;

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