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