let x, y be Real; :: thesis: ( (min (x,y)) * (max (x,y)) = x * y & (min (x,y)) + (max (x,y)) = x + y )

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

suppose x >= y ; :: thesis: ( (min (x,y)) * (max (x,y)) = x * y & (min (x,y)) + (max (x,y)) = x + y )

then ( min (x,y) = y & max (x,y) = x ) by XXREAL_0:def 9, XXREAL_0:def 10;
hence ( (min (x,y)) * (max (x,y)) = x * y & (min (x,y)) + (max (x,y)) = x + y ) ; :: thesis: verum

end;

suppose x < y ; :: thesis: ( (min (x,y)) * (max (x,y)) = x * y & (min (x,y)) + (max (x,y)) = x + y )

then ( min (x,y) = x & max (x,y) = y ) by XXREAL_0:def 9, XXREAL_0:def 10;
hence ( (min (x,y)) * (max (x,y)) = x * y & (min (x,y)) + (max (x,y)) = x + y ) ; :: thesis: verum

end;

end;