theorem :: XREAL_1:160

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