let x, y be real number ; :: thesis: max x,y = ((x + y) + |.(x - y).|) / 2

per cases ( y <= x or x <= y ) ;

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

hence max x,y = ((x + y) + (x - y)) / 2 by XXREAL_0:def 10
.= ((x + y) + |.(x - y).|) / 2 by A1, Th129, XREAL_1:50 ;
:: thesis: verum

end;

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

then A3: 0 <= y - x by XREAL_1:50;
thus max x,y = ((x + y) + (- (x - y))) / 2 by A2, XXREAL_0:def 10
.= ((x + y) + |.(- (x - y)).|) / 2 by A3, Th129
.= ((x + y) + |.(x - y).|) / 2 by Lm22 ; :: thesis: verum

end;

end;