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);
(- d) + (abs d) >= 0 by ABSVALUE:27;
then (- 2) * (((((- d) + (abs d)) + 4) + (((- d) + (abs d)) + 4)) + (((- d) + (abs d)) + 4)) < (- 2) * 0 by XREAL_1:69;
then A1: ((- 2) * (((((- d) + (abs d)) + 4) + (((- d) + (abs d)) + 4)) + (((- d) + (abs d)) + 4))) / 4 < 0 / 4 by XREAL_1:74;
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 d + (abs d) = ((- 2) * (((((- d) + (abs d)) + 4) + (((- d) + (abs d)) + 4)) + (((- d) + (abs d)) + 4))) / 4 ;
hence contradiction by A1, ABSVALUE:26; :: thesis: verum