let a, b, c, d be positive Real; :: thesis: ( a + b <= c + d & a * b > c * d implies ( max (a,b) < max (c,d) & min (a,b) > min (c,d) ) )
A1: ( a + b = (max (a,b)) + (min (a,b)) & c + d = (max (c,d)) + (min (c,d)) & a * b = (max (a,b)) * (min (a,b)) & c * d = (max (c,d)) * (min (c,d)) ) by NEWTON04:18;
assume A2: ( a + b <= c + d & a * b > c * d ) ; :: thesis: ( max (a,b) < max (c,d) & min (a,b) > min (c,d) )
then max (a,b) <= max (c,d) by SMI;

per cases then ( max (a,b) = max (c,d) or max (a,b) < max (c,d) ) by XXREAL_0:1;

suppose B1: max (a,b) = max (c,d) ; :: thesis: ( max (a,b) < max (c,d) & min (a,b) > min (c,d) )

then min (a,b) <= min (c,d) by A1, A2, XREAL_1:6;
hence ( max (a,b) < max (c,d) & min (a,b) > min (c,d) ) by A2, B1, A1, XREAL_1:64; :: thesis: verum

end;

suppose max (a,b) < max (c,d) ; :: thesis: ( max (a,b) < max (c,d) & min (a,b) > min (c,d) )

hence ( max (a,b) < max (c,d) & min (a,b) > min (c,d) ) by A1, A2, XREAL_1:66; :: thesis: verum

end;

end;