let b, d be Real; :: thesis: b + 1 <> b + ((((- d) + |.d.|) + 4) + d)
set c = ((- d) + |.d.|) + 4;
|.d.| >= 0 by COMPLEX1:46;
then A1: |.d.| + 3 >= 0 + 3 by XREAL_1:7;
assume b + 1 = b + ((((- d) + |.d.|) + 4) + d) ; :: thesis: contradiction
hence contradiction by A1; :: thesis: verum