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

now :: thesis: ( r is not Integer implies 0 < frac r )

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

end;

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