for n being Nat st n > 1 holds
((((2 * n) -' 2) !) * n) * (n + 1) < (2 * n) !