let c, d be real number ; :: thesis: ( c > 0 implies (((abs d) + c) + c) + 1 <> - (((abs d) + c) + d) )
assume A1: c > 0 ; :: thesis: (((abs d) + c) + c) + 1 <> - (((abs d) + c) + d)
assume A2: (((abs d) + c) + c) + 1 = - (((abs d) + c) + d) ; :: thesis: contradiction

per cases ( d >= 0 or d < 0 ) ;

suppose A3: d >= 0 ; :: thesis: contradiction

then abs d = d by ABSVALUE:def 1;
then A4: ((3 * d) + (3 * c)) + 1 = 0 by A2;
A5: 3 * d >= 3 * 0 by A3;
3 * c >= 3 * 0 by A1;
then (3 * d) + (3 * c) >= 0 + 0 by A5;
hence contradiction by A4; :: thesis: verum

end;

suppose A6: d < 0 ; :: thesis: contradiction

then abs d = - d by ABSVALUE:def 1;
then A7: ((- d) + (3 * c)) + 1 = 0 by A2;
A8: - d > - 0 by A6, XREAL_1:26;
3 * c >= 3 * 0 by A1;
then (- d) + (3 * c) >= 0 + 0 by A8;
hence contradiction by A7; :: thesis: verum

end;

end;