theorem :: XREAL_1:213

for a being Real st a <= - 1 holds
- 1 <= a "