let c, d be real number ; :: thesis: ( c > 0 implies ((abs d) + c) + 1 <> - ((((abs d) + c) + c) + d) )
assume A1: c > 0 ; :: thesis: ((abs d) + c) + 1 <> - ((((abs d) + c) + c) + d)
assume A2: ((abs d) + c) + 1 = - ((((abs d) + c) + 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;
hence contradiction by A1, A2, A3; :: thesis: verum

end;

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

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

end;

end;