let a, b be Real; :: thesis: max (a,b) = ((a + b) + |.(a - b).|) / 2

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

suppose A1: b <= a ; :: thesis: max (a,b) = ((a + b) + |.(a - b).|) / 2

hence max (a,b) = ((a + b) + (a - b)) / 2 by XXREAL_0:def 10
.= ((a + b) + |.(a - b).|) / 2 by A1, Th43, XREAL_1:48 ;
:: thesis: verum

end;

suppose A2: a <= b ; :: thesis: max (a,b) = ((a + b) + |.(a - b).|) / 2

then A3: 0 <= b - a by XREAL_1:48;
thus max (a,b) = ((a + b) + (- (a - b))) / 2 by A2, XXREAL_0:def 10
.= ((a + b) + |.(- (a - b)).|) / 2 by A3, Th43
.= ((a + b) + |.(a - b).|) / 2 by Lm26 ; :: thesis: verum

end;

end;