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