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