let n be Nat; :: thesis: ( n > 1 implies n < (2 * n) -' 1 )
assume A1: n > 1 ; :: thesis: n < (2 * n) -' 1
then n + n > n + 1 by XREAL_1:6;
then A2: (n + n) - 1 > (n + 1) - 1 by XREAL_1:9;
1 * 2 < 2 * n by A1, XREAL_1:68;
hence n < (2 * n) -' 1 by A2, XREAL_1:233, XXREAL_0:2; :: thesis: verum