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