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

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

hence
( 1 < denominator p iff not p is integer )
by Th14; :: thesis: verumassume 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;denominator p >= 1 by Th8;

hence denominator p > 1 by A1, Th15, XXREAL_0:1; :: thesis: verum