let n be non zero natural number ; :: thesis: not Radical n is square-containing
assume Radical n is square-containing ; :: thesis: contradiction
then ex p being Prime st p |^ 2 divides Radical n by Def1;
hence contradiction by Lm3; :: thesis: verum