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