let r be Rational; :: thesis: ( r |^ 3 >= 0 iff r >= 0 )
r |^ 3 = r |^ (2 + 1)
.= (r |^ (1 + 1)) * r by NEWTON:6
.= ((r |^ 1) * r) * r by NEWTON:6
.= (r * r) * r ;
hence ( r |^ 3 >= 0 iff r >= 0 ) ; :: thesis: verum