theorem Th3: :: BORSUK_7:3

for r, s being Real st frac r < frac s holds
frac (r - s) = ((frac r) - (frac s)) + 1