theorem :: INT_1:46

for r being Real holds
( 0 < frac r iff not r is integer )