theorem Th41: :: INT_1:43

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