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 a < b ; :: thesis: a / c < b / c
then a * (c ") < b * (c ") by A1, Lm13;
then a / c < b * (c ") by XCMPLX_0:def 9;
hence a / c < b / c by XCMPLX_0:def 9; :: thesis: verum