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