let x be real number ; :: thesis: (- x) |^ 3 = - (x |^ 3)
3 = (2 * 1) + 1 ;
then not 3 is even by ABIAN:1;
hence (- x) |^ 3 = - (x |^ 3) by POWER:2; :: thesis: verum