let k, n be non zero natural number ; :: thesis: ( ( k divides n & not k is square-containing ) iff k divides Radical n )
A1: ( k divides Radical n implies ( k divides n & not k is square-containing ) )

proof

assume A2: k divides Radical n ; :: thesis: ( k divides n & not k is square-containing )
Radical n divides n by Th55;
hence ( k divides n & not k is square-containing ) by A2, Th26, NAT_D:4; :: thesis: verum

end;

( k is non zero Element of NAT & n is non zero Element of NAT ) by ORDINAL1:def 13;
hence ( ( k divides n & not k is square-containing ) iff k divides Radical n ) by A1, Lm5; :: thesis: verum