theorem Th3: :: EUCLID_9:3

for f, g being complex-valued Function holds abs (f - g) = abs (g - f)