let a, b be real number ; :: thesis: ( 0 <= a & a < b implies a / b < 1 )
assume that
A1: 0 <= a and
A2: a < b ; :: thesis: a / b < 1
a / b < b / b by A1, A2, Lm26;
hence a / b < 1 by A1, A2, XCMPLX_1:60; :: thesis: verum