let a, b be Real; :: thesis: ( 0 < a & a < b implies 1 < b / a )
assume A1: a > 0 ; :: thesis: ( not a < b or 1 < b / a )
assume A2: a < b ; :: thesis: 1 < b / a
assume b / a <= 1 ; :: thesis: contradiction
then (b / a) * a <= 1 * a by A1, Lm12;
hence contradiction by A1, A2, XCMPLX_1:87; :: thesis: verum