let n be non zero natural number ; :: thesis: not Radical n is square-containing
assume Radical n is square-containing ; :: thesis: contradiction
then consider p being Prime such that
A1: p |^ 2 divides Radical n by Def1;
thus contradiction by A1, Lm3; :: thesis: verum