for r being Real holds
( frac r < 1 & 0 <= frac r )