let a, b, c be Real; :: thesis: ( c <= 0 & b / c < a / c implies a < b )
assume that
A1: c <= 0 and
A2: b / c < a / c ; :: thesis: a < b

A3: now :: thesis: not c = 0

assume c = 0 ; :: thesis: contradiction
then A4: c " = 0 ;
a / c = a * (c ") by XCMPLX_0:def 9
.= b * (c ") by A4
.= b / c by XCMPLX_0:def 9 ;
hence contradiction by A2; :: thesis: verum

end;

then (a / c) * c < (b / c) * c by A1, A2, Lm24;
then a < (b / c) * c by A3, XCMPLX_1:87;
hence a < b by A3, XCMPLX_1:87; :: thesis: verum