let x, y, z be real number ; :: thesis: ( x > y & y > z implies (((x ^2 ) * y) + ((y ^2 ) * z)) + ((z ^2 ) * x) > ((x * (y ^2 )) + (y * (z ^2 ))) + (z * (x ^2 )) )
assume A1: ( x > y & y > z ) ; :: thesis: (((x ^2 ) * y) + ((y ^2 ) * z)) + ((z ^2 ) * x) > ((x * (y ^2 )) + (y * (z ^2 ))) + (z * (x ^2 ))
then A2: ( x - y > 0 & y - z > 0 ) by XREAL_1:52;
x > z by A1, XXREAL_0:2;
then A3: x - z > 0 by XREAL_1:52;
(x - y) * (y - z) > 0 by A2;
then ((x - y) * (y - z)) * (x - z) > 0 by A3;
then ((((x ^2 ) * y) + ((y ^2 ) * z)) + ((z ^2 ) * x)) - (((x * (y ^2 )) + (y * (z ^2 ))) + (z * (x ^2 ))) > 0 ;
hence (((x ^2 ) * y) + ((y ^2 ) * z)) + ((z ^2 ) * x) > ((x * (y ^2 )) + (y * (z ^2 ))) + (z * (x ^2 )) by XREAL_1:49; :: thesis: verum