theorem :: XREAL_1:161

for a, b being Real st 1 < a & 1 <= b holds
1 < a * b