let d be real number ; :: thesis: ((((abs d) + (((- d) + (abs d)) + 4)) + 2) - 2) + d <> - ((((((abs d) + (((- d) + (abs d)) + 4)) + (((- d) + (abs d)) + 4)) + 2) - 2) + d)
set c = ((- d) + (abs d)) + 4;
set xx = ((((- d) + (abs d)) + 4) + (((- d) + (abs d)) + 4)) + (((- d) + (abs d)) + 4);
assume ((((abs d) + (((- d) + (abs d)) + 4)) + 2) - 2) + d = - ((((((abs d) + (((- d) + (abs d)) + 4)) + (((- d) + (abs d)) + 4)) + 2) - 2) + d) ; :: thesis: contradiction
then A1: d + (abs d) = ((- 2) * (((((- d) + (abs d)) + 4) + (((- d) + (abs d)) + 4)) + (((- d) + (abs d)) + 4))) / 4 ;
(- d) + (abs d) >= 0 by ABSVALUE:44;
then ((- d) + (abs d)) + 4 >= 0 + 4 by XREAL_1:8;
then 3 * (((- d) + (abs d)) + 4) > 3 * 0 by XREAL_1:70;
then (- 2) * (((((- d) + (abs d)) + 4) + (((- d) + (abs d)) + 4)) + (((- d) + (abs d)) + 4)) < (- 2) * 0 by XREAL_1:71;
then ((- 2) * (((((- d) + (abs d)) + 4) + (((- d) + (abs d)) + 4)) + (((- d) + (abs d)) + 4))) / 4 < 0 / 4 by XREAL_1:76;
hence contradiction by A1, ABSVALUE:43; :: thesis: verum