let x, y, z be Real; ( x > y & y > z implies (((x ^2) * y) + ((y ^2) * z)) + ((z ^2) * x) > ((x * (y ^2)) + (y * (z ^2))) + (z * (x ^2)) )
assume that
A1:
x > y
and
A2:
y > z
; (((x ^2) * y) + ((y ^2) * z)) + ((z ^2) * x) > ((x * (y ^2)) + (y * (z ^2))) + (z * (x ^2))
A3:
y - z > 0
by A2, XREAL_1:50;
x > z
by A1, A2, XXREAL_0:2;
then A4:
x - z > 0
by XREAL_1:50;
x - y > 0
by A1, XREAL_1:50;
then
((x - y) * (y - z)) * (x - z) > 0
by A3, A4;
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:47; verum