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