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