let x, y be R_eal; :: thesis: |.(x - y).| = |.(y - x).|
|.(y - x).| = |.(- (x - y)).| by XXREAL_3:26;
hence |.(x - y).| = |.(y - x).| by EXTREAL1:29; :: thesis: verum