let d be Real; :: thesis: (((|.d.| + (((- d) + |.d.|) + 4)) + 2) - 2) + d <> - (((((|.d.| + (((- d) + |.d.|) + 4)) + (((- d) + |.d.|) + 4)) + 2) - 2) + d)
set c = ((- d) + |.d.|) + 4;
set xx = ((((- d) + |.d.|) + 4) + (((- d) + |.d.|) + 4)) + (((- d) + |.d.|) + 4);
(- d) + |.d.| >= 0 by ABSVALUE:27;
then (- 2) * (((((- d) + |.d.|) + 4) + (((- d) + |.d.|) + 4)) + (((- d) + |.d.|) + 4)) < (- 2) * 0 by XREAL_1:69;
then A1: ((- 2) * (((((- d) + |.d.|) + 4) + (((- d) + |.d.|) + 4)) + (((- d) + |.d.|) + 4))) / 4 < 0 / 4 by XREAL_1:74;
assume (((|.d.| + (((- d) + |.d.|) + 4)) + 2) - 2) + d = - (((((|.d.| + (((- d) + |.d.|) + 4)) + (((- d) + |.d.|) + 4)) + 2) - 2) + d) ; :: thesis: contradiction
then d + |.d.| = ((- 2) * (((((- d) + |.d.|) + 4) + (((- d) + |.d.|) + 4)) + (((- d) + |.d.|) + 4))) / 4 ;
hence contradiction by A1, ABSVALUE:26; :: thesis: verum