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

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

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

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

end;

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

hence min x,y = ((x + y) - (x - y)) / 2 by XXREAL_0:def 9
.= ((x + y) - |.(x - y).|) / 2 by A2, Th129, XREAL_1:50 ;
:: thesis: verum

end;

end;