let r, s be real number ; :: thesis: abs (r - s) = abs (s - r)

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

suppose r > s ; :: thesis: abs (r - s) = abs (s - r)

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

end;

suppose r = s ; :: thesis: abs (r - s) = abs (s - r)

hence abs (r - s) = abs (s - r) ; :: thesis: verum

end;

suppose r < s ; :: thesis: abs (r - s) = abs (s - r)

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

end;

end;