theorem :: XREAL_1:150

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