let c, d be Real; :: thesis: ( c > 0 implies (|.d.| + c) + 1 <> - (((|.d.| + c) + c) + d) )
assume A1: c > 0 ; :: thesis: (|.d.| + c) + 1 <> - (((|.d.| + c) + c) + d)
assume A2: (|.d.| + c) + 1 = - (((|.d.| + c) + c) + d) ; :: thesis: contradiction

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

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

then |.d.| = d by ABSVALUE:def 1;
hence contradiction by A1, A2, A3; :: thesis: verum

end;

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

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

end;

end;