let a be Real; :: thesis: ex b being Real st b < a
take a - 1 ; :: thesis: a - 1 < a
a + (- 1) < a + (- 0) by Lm8;
hence a - 1 < a ; :: thesis: verum