let a, b be Element of [.0,1.]; :: thesis: min ((a + b),1) = 1 - (max (0,(((1 - a) + (1 - b)) - 1)))

per cases ( a + b <= 1 or a + b > 1 ) ;

suppose A1: a + b <= 1 ; :: thesis: min ((a + b),1) = 1 - (max (0,(((1 - a) + (1 - b)) - 1)))

then A2: (a + b) - (a + b) <= 1 - (a + b) by XREAL_1:9;
min ((a + b),1) = 1 - ((1 - a) - b) by A1, XXREAL_0:def 9
.= 1 - (max (0,(((1 - a) + (1 - b)) - 1))) by A2, XXREAL_0:def 10 ;
hence min ((a + b),1) = 1 - (max (0,(((1 - a) + (1 - b)) - 1))) ; :: thesis: verum

end;

suppose A1: a + b > 1 ; :: thesis: min ((a + b),1) = 1 - (max (0,(((1 - a) + (1 - b)) - 1)))

then A2: (a + b) - (a + b) > 1 - (a + b) by XREAL_1:9;
min ((a + b),1) = 1 - 0 by A1, XXREAL_0:def 9
.= 1 - (max (0,(((1 - a) + (1 - b)) - 1))) by A2, XXREAL_0:def 10 ;
hence min ((a + b),1) = 1 - (max (0,(((1 - a) + (1 - b)) - 1))) ; :: thesis: verum

end;

end;