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

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