let r be real number ; :: thesis: ( 0 < frac r iff not r is integer )

now

assume r is not Integer ; :: thesis: 0 < frac r
then 0 <> frac r ;
hence 0 < frac r by Th69; :: thesis: verum

end;

hence ( 0 < frac r iff not r is integer ) by Th71; :: thesis: verum