theorem :: XREAL_1:88

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