theorem :: XREAL_1:149

for a being Real st a < 1 holds
1 - a > 0 by Lm21;