let n be Nat; :: thesis: (2 |^ (n + 2)) + ((- 1) |^ (n + 2)) > 0
A1: ( (- 1) |^ (n + 2) = |.((- 1) |^ (n + 2)).| or - ((- 1) |^ (n + 2)) = |.((- 1) |^ (n + 2)).| ) by ABSVALUE:1;
A2: |.((- 1) |^ (n + 2)).| = 1 by Th1;
n + 2 >= 2 by NAT_1:11;
then n + 2 > 0 by XXREAL_0:2;
then 2 |^ (n + 2) > 1 by PEPIN:25;
then A3: (2 |^ (n + 2)) + ((- 1) |^ (n + 2)) > 1 + ((- 1) |^ (n + 2)) by XREAL_1:8;

per cases ( (- 1) |^ (n + 2) = - 1 or (- 1) |^ (n + 2) = 1 ) by A2, A1;

suppose (- 1) |^ (n + 2) = - 1 ; :: thesis: (2 |^ (n + 2)) + ((- 1) |^ (n + 2)) > 0

hence (2 |^ (n + 2)) + ((- 1) |^ (n + 2)) > 0 by A3; :: thesis: verum

end;

suppose (- 1) |^ (n + 2) = 1 ; :: thesis: (2 |^ (n + 2)) + ((- 1) |^ (n + 2)) > 0

hence (2 |^ (n + 2)) + ((- 1) |^ (n + 2)) > 0 by A3, XXREAL_0:2; :: thesis: verum

end;

end;