assume not n -root a is heavy ; :: thesis: contradiction
then not (n -root a) |^ n is heavy ;
hence contradiction by POLYEQ_5:7; :: thesis: verum