theorem :: XREAL_1:89

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