let a, b be Real; :: thesis: min (a,b) = ((a + b) - |.(a - b).|) / 2
per cases ( a <= b or b <= a ) ;
suppose A1: a <= b ; :: thesis: min (a,b) = ((a + b) - |.(a - b).|) / 2
|.(a - b).| = |.(- (b - a)).|
.= |.(b - a).| by Lm26
.= b - a by A1, Th43, XREAL_1:48 ;
hence min (a,b) = ((a + b) - |.(a - b).|) / 2 by A1, XXREAL_0:def 9; :: thesis: verum
end;
suppose A2: b <= a ; :: thesis: min (a,b) = ((a + b) - |.(a - b).|) / 2
hence min (a,b) = ((a + b) - (a - b)) / 2 by XXREAL_0:def 9
.= ((a + b) - |.(a - b).|) / 2 by A2, Th43, XREAL_1:48 ;
:: thesis: verum
end;
end;