let x, y be R_eal; :: thesis: |.(x - y).| = |.(y - x).|
|.(y - x).| = |.(- (x - y)).| by XXREAL_3:27;
hence |.(x - y).| = |.(y - x).| by EXTREAL2:66; :: thesis: verum