theorem F51max: :: FUZZY_8:5

for a, b, c being Real holds |.((max (c,a)) - (max (c,b))).| <= |.(a - b).|