let r, s be Real; :: thesis: ( abs (r - s) = 0 iff r = s )

hereby :: thesis: ( r = s implies abs (r - s) = 0 )

assume abs (r - s) = 0 ; :: thesis: r = s
then r - s = 0 by ABSVALUE:2;
hence r = s ; :: thesis: verum

end;

assume r = s ; :: thesis: abs (r - s) = 0
hence abs (r - s) = 0 by ABSVALUE:2; :: thesis: verum