let x be natural number ; :: thesis: ( x is n + 1 _or_greater implies x is n _or_greater )
assume A1: x is n + 1 _or_greater ; :: thesis: x is n _or_greater
n + 1 >= n + 0 by XREAL_1:6;
hence x is n _or_greater by A1, XXREAL_0:2; :: thesis: verum