theorem Th4: :: BORSUK_7:4

for r, s being Real ex i being Integer st
( frac (r - s) = ((frac r) - (frac s)) + i & ( i = 0 or i = 1 ) )