let x, y, z, s be ExtReal; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum

assume that

A1: 0 <= x and

A2: x <= y and

A3: 0 <= s and

A4: s <= z ; :: thesis: 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; :: thesis: verum