theorem Th2: :: JCT_MISC:2

for r, s, r0, s0 being Real holds |.(|.(r0 - s0).| - |.(r - s).|).| <= |.(r0 - r).| + |.(s0 - s).|