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

hereby :: thesis: ( r = s implies |.(r - s).| = 0 )

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

end;

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