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

end;

end;