let a, b, c, d be positive Real; :: thesis: ( a + b <= c + d & max (a,b) > max (c,d) implies a * b < 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)) & (max (c,d)) * (min (c,d)) = c * d ) by NEWTON04:18;
assume A2: ( a + b <= c + d & max (a,b) > max (c,d) ) ; :: thesis: a * b < c * d
then A4: ((max (a,b)) + (min (a,b))) * ((max (a,b)) + (min (a,b))) <= ((max (c,d)) + (min (c,d))) * ((max (c,d)) + (min (c,d))) by A1, XREAL_1:66;
min (a,b) < min (c,d) by A1, A2, XREAL_1:8;
then ( (max (a,b)) * (max (a,b)) > (max (c,d)) * (max (c,d)) & (min (a,b)) * (min (a,b)) < (min (c,d)) * (min (c,d)) ) by A2, XREAL_1:96;
then ((max (a,b)) * (max (a,b))) - ((min (a,b)) * (min (a,b))) > ((max (c,d)) * (max (c,d))) - ((min (c,d)) * (min (c,d))) by XREAL_1:14;
then ((max (a,b)) - (min (a,b))) * ((max (a,b)) + (min (a,b))) > ((max (c,d)) - (min (c,d))) * ((max (c,d)) + (min (c,d))) ;
then (max (a,b)) - (min (a,b)) > (max (c,d)) - (min (c,d)) by A1, A2, XREAL_1:66;
then ((max (a,b)) - (min (a,b))) * ((max (a,b)) - (min (a,b))) > ((max (c,d)) - (min (c,d))) * ((max (c,d)) - (min (c,d))) by XREAL_1:96;
then (((max (a,b)) + (min (a,b))) * ((max (a,b)) + (min (a,b)))) - (((max (a,b)) - (min (a,b))) * ((max (a,b)) - (min (a,b)))) < (((max (c,d)) + (min (c,d))) * ((max (c,d)) + (min (c,d)))) - (((max (c,d)) - (min (c,d))) * ((max (c,d)) - (min (c,d)))) by A4, XREAL_1:15;
then 4 * ((max (a,b)) * (min (a,b))) < 4 * ((max (c,d)) * (min (c,d))) ;
hence a * b < c * d by A1, XREAL_1:64; :: thesis: verum