theorem :: XREAL_1:212

for a being Real st 1 < a holds
a " < 1 by Lm36;