theorem :: XREAL_1:191

for a, b being Real st 0 < a & b < a holds
b / a < 1