(- a) |^ n is positive ;
then - (a |^ n) is positive by POWER:2;
hence a |^ n is negative ; :: thesis: verum