let c, a, b be real number ; :: thesis: ( 0 < c & 0 < a & a < b implies c / b < c / a )
assume that
A1: 0 < c and
A2: 0 < a and
A3: a < b ; :: thesis: c / b < c / a
a * (b " ) < b * (b " ) by A2, A3, Lm13;
then a * (b " ) < 1 by A2, A3, XCMPLX_0:def 7;
then (a " ) * (a * (b " )) < (a " ) * 1 by A2, Lm13;
then ((a " ) * a) * (b " ) < a " ;
then 1 * (b " ) < a " by A2, XCMPLX_0:def 7;
then c * (b " ) < c * (a " ) by A1, Lm13;
then c / b < c * (a " ) by XCMPLX_0:def 9;
hence c / b < c / a by XCMPLX_0:def 9; :: thesis: verum