theorem Th5: :: NTALGO_1:5

for x, y being Element of INT st |.y.| <> 0 holds
|.(x mod y).| < |.y.|