let a, b, c be Real; :: thesis: ( c <= 0 & 0 < a & a <= b implies c / a <= c / b )
assume A1: c <= 0 ; :: thesis: ( not 0 < a or not a <= b or c / a <= c / b )
assume that
A2: a > 0 and
A3: a <= b ; :: thesis: c / a <= c / b
a " >= b " by A2, A3, Lm32;
then (a ") * c <= (b ") * c by A1, Lm28;
then c / a <= (b ") * c by XCMPLX_0:def 9;
hence c / a <= c / b by XCMPLX_0:def 9; :: thesis: verum