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