let x, y, z, s be ExtReal; ( 0 <= x & x <= y & 0 <= s & s <= z implies x * s <= y * z )
assume that
A1:
0 <= x
and
A2:
x <= y
and
A3:
0 <= s
and
A4:
s <= z
; x * s <= y * z
A5:
x * s <= y * s
by A2, A3, XXREAL_3:71;
y * s <= y * z
by A1, A2, A4, XXREAL_3:71;
hence
x * s <= y * z
by A5, XXREAL_0:2; verum