let c, a, b be real number ; :: thesis: ( 0 < c & a < b implies a / c < b / c )
assume 0 < c ; :: thesis: ( not a < b or a / c < b / c )
then A1: 0 < c " ;
( a < b implies a / c < b / c )

proof

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

end;

hence ( not a < b or a / c < b / c ) ; :: thesis: verum