let n be non zero Nat; :: thesis: Radical n is square-free
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