let f, g be complex-valued Function; :: thesis: abs (f - g) = abs (g - f)
f - g = - (g - f) by VALUED_2:18;
hence abs (f - g) = abs (g - f) by EUCLID:5; :: thesis: verum