let n be Element of NAT ; :: thesis: (2 |^ (n + 2)) + ((- 1) |^ (n + 2)) > 0
n + 2 >= 2 by NAT_1:11;
then n + 2 > 0 by XXREAL_0:2;
then 2 |^ (n + 2) > 1 by PEPIN:26;
then A1: (2 |^ (n + 2)) + ((- 1) |^ (n + 2)) > 1 + ((- 1) |^ (n + 2)) by XREAL_1:10;
A2: abs ((- 1) |^ (n + 2)) = 1 by Th1;
A3: ( (- 1) |^ (n + 2) = abs ((- 1) |^ (n + 2)) or - ((- 1) |^ (n + 2)) = abs ((- 1) |^ (n + 2)) ) by ABSVALUE:1;

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

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

hence (2 |^ (n + 2)) + ((- 1) |^ (n + 2)) > 0 by A1; :: 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 A1, XXREAL_0:2; :: thesis: verum

end;

end;