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

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

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

assume
r = s
; :: thesis: |.(r - s).| = 0 assume
|.(r - s).| = 0
; :: thesis: r = s

then r - s = 0 by ABSVALUE:2;

hence r = s ; :: thesis: verum

end;then r - s = 0 by ABSVALUE:2;

hence r = s ; :: thesis: verum

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