let c, b, a be real number ; :: 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

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, Lm25;
then a < (b / c) * c by A3, XCMPLX_1:88;
hence a < b by A3, XCMPLX_1:88; :: thesis: verum