theorem :: INT_1:45

for r being Real holds
( frac r = 0 iff r is integer ) ;