let n, k be non zero Nat; :: thesis: ( k <> 1 & k ^2 divides n implies n is square-containing )
assume A1: ( k <> 1 & k ^2 divides n ) ; :: thesis: n is square-containing
then k |^ 2 divides n by NEWTON:81;
hence n is square-containing by A1, MOEBIUS1:20; :: thesis: verum