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;