let a be Real; :: thesis: a - 1 < a
a + (- 1) < a + 0 by Lm10;
hence a - 1 < a ; :: thesis: verum