theorem Th1: :: MESFUNC5:1

for x, y being R_eal holds |.(x - y).| = |.(y - x).|