theorem Th155: :: XREAL_1:155

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