theorem :: XREAL_1:85

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