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 EXTREAL2:18; :: thesis: verum