for a being Real
for n being Nat st ( a >= 0 or n is even ) holds
a |^ n >= 0