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