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

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

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

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

end;

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

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

end;

end;