let a, b, c be Real; :: thesis: ( 0 < c & a < b implies a * c < b * c )
assume A1: 0 < c ; :: thesis: ( not a < b or a * c < b * c )
assume A2: a < b ; :: thesis: a * c < b * c
A3: a * c <> b * c
proof
assume a * c = b * c ; :: thesis: contradiction
then a * (c * (c ")) = (b * c) * (c ") by XCMPLX_1:4;
then a * 1 = b * (c * (c ")) by A1, XCMPLX_0:def 7;
then a = b * 1 by A1, XCMPLX_0:def 7;
hence contradiction by A2; :: thesis: verum
end;
a * c <= b * c by A1, A2, Lm12;
hence a * c < b * c by A3, XXREAL_0:1; :: thesis: verum