let a, b, c be Element of [.0,1.]; :: thesis: max (0,(((max (0,((a + b) - 1))) + c) - 1)) = max (0,((a + (max (0,((b + c) - 1)))) - 1))
A1: ( 0 <= a & 0 <= b & 0 <= c ) by XXREAL_1:1;
zz: c - 0 <= 1 by XXREAL_1:1;
then c - 1 <= 0 by XREAL_1:12;
then y2: (c - 1) + ((a + b) - 1) <= 0 + ((a + b) - 1) by XREAL_1:6;

per cases ( ( 0 <= (a + b) - 1 & 0 <= (b + c) - 1 ) or ( 0 > (a + b) - 1 & 0 <= (b + c) - 1 ) or ( 0 > (a + b) - 1 & 0 > (b + c) - 1 ) or ( 0 <= (a + b) - 1 & 0 > (b + c) - 1 ) ) ;

suppose Z0: ( 0 <= (a + b) - 1 & 0 <= (b + c) - 1 ) ; :: thesis: max (0,(((max (0,((a + b) - 1))) + c) - 1)) = max (0,((a + (max (0,((b + c) - 1)))) - 1))

then Z1: max (0,((a + b) - 1)) = (a + b) - 1 by XXREAL_0:def 10;
max (0,((b + c) - 1)) = (b + c) - 1 by Z0, XXREAL_0:def 10;
hence max (0,(((max (0,((a + b) - 1))) + c) - 1)) = max (0,((a + (max (0,((b + c) - 1)))) - 1)) by Z1; :: thesis: verum

end;

suppose Z0: ( 0 > (a + b) - 1 & 0 <= (b + c) - 1 ) ; :: thesis: max (0,(((max (0,((a + b) - 1))) + c) - 1)) = max (0,((a + (max (0,((b + c) - 1)))) - 1))

then Z1: max (0,((a + b) - 1)) = 0 by XXREAL_0:def 10;
Z2: max (0,((b + c) - 1)) = (b + c) - 1 by Z0, XXREAL_0:def 10;
max (0,(((max (0,((a + b) - 1))) + c) - 1)) = 0 by zz, XXREAL_0:def 10, Z1, XREAL_1:12
.= max (0,((a + (max (0,((b + c) - 1)))) - 1)) by Z2, y2, Z0, XXREAL_0:def 10 ;
hence max (0,(((max (0,((a + b) - 1))) + c) - 1)) = max (0,((a + (max (0,((b + c) - 1)))) - 1)) ; :: thesis: verum

end;

suppose Z0: ( 0 > (a + b) - 1 & 0 > (b + c) - 1 ) ; :: thesis: max (0,(((max (0,((a + b) - 1))) + c) - 1)) = max (0,((a + (max (0,((b + c) - 1)))) - 1))

then Z3: ( c - 1 < 0 & a - 1 < 0 ) by XREAL_1:9, A1, XREAL_1:31;
Z1: max (0,((a + b) - 1)) = 0 by Z0, XXREAL_0:def 10;
Z2: max (0,((b + c) - 1)) = 0 by Z0, XXREAL_0:def 10;
max (0,(((max (0,((a + b) - 1))) + c) - 1)) = 0 by Z3, XXREAL_0:def 10, Z1
.= max (0,((a + (max (0,((b + c) - 1)))) - 1)) by Z2, Z3, XXREAL_0:def 10 ;
hence max (0,(((max (0,((a + b) - 1))) + c) - 1)) = max (0,((a + (max (0,((b + c) - 1)))) - 1)) ; :: thesis: verum

end;

suppose Z0: ( 0 <= (a + b) - 1 & 0 > (b + c) - 1 ) ; :: thesis: max (0,(((max (0,((a + b) - 1))) + c) - 1)) = max (0,((a + (max (0,((b + c) - 1)))) - 1))

ds: a - 0 <= 1 by XXREAL_1:1;
then a - 1 <= 0 by XREAL_1:12;
then sb: (a - 1) + ((b + c) - 1) <= 0 + 0 by Z0;
Z1: max (0,((a + b) - 1)) = (a + b) - 1 by Z0, XXREAL_0:def 10;
max (0,(((max (0,((a + b) - 1))) + c) - 1)) = 0 by sb, XXREAL_0:def 10, Z1
.= max (0,((a + 0) - 1)) by XXREAL_0:def 10, XREAL_1:12, ds
.= max (0,((a + (max (0,((b + c) - 1)))) - 1)) by Z0, XXREAL_0:def 10 ;
hence max (0,(((max (0,((a + b) - 1))) + c) - 1)) = max (0,((a + (max (0,((b + c) - 1)))) - 1)) ; :: thesis: verum

end;

end;