let a, b be real number ; :: thesis: ( 0 < a & a <= b implies 1 <= b / a )
assume A1: ( 0 < a & a <= b ) ; :: thesis: 1 <= b / a
then b / a >= a / a by Lm27;
hence b / a >= 1 by A1, XCMPLX_1:60; :: thesis: verum