let r, s be Real; :: thesis: |.(r - s).| = |.(s - r).|

per cases ( r > s or r = s or r < s ) by XXREAL_0:1;

suppose r > s ; :: thesis: |.(r - s).| = |.(s - r).|

then s - r < 0 by XREAL_1:49;
then |.(s - r).| = - (s - r) by ABSVALUE:def 1
.= r - s ;
hence |.(r - s).| = |.(s - r).| ; :: thesis: verum

end;

suppose r = s ; :: thesis: |.(r - s).| = |.(s - r).|

hence |.(r - s).| = |.(s - r).| ; :: thesis: verum

end;

suppose r < s ; :: thesis: |.(r - s).| = |.(s - r).|

then r - s < 0 by XREAL_1:49;
then |.(r - s).| = - (r - s) by ABSVALUE:def 1
.= s - r ;
hence |.(r - s).| = |.(s - r).| ; :: thesis: verum

end;

end;