theorem :: XREAL_1:159

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