theorem LmSin2: :: FUZZY_5:3
for x, y being Real holds |.((sin x) - (sin y)).| <= |.(x - y).|