let a, b be Real; :: thesis: ( 0 < a & 1 < b implies (a / b) - a < 0 )
assume that
A1: 0 < a and
A2: 1 < b ; :: thesis: (a / b) - a < 0
A3: (a / b) - a = a * ((1 / b) - 1) ;
(1 / b) - 1 < 0 by A2, Th07;
hence (a / b) - a < 0 by A1, A3; :: thesis: verum