let n be non zero natural number ; :: thesis: for p being Prime holds not p |^ 2 divides Radical n
let p be Prime; :: thesis: not p |^ 2 divides Radical n
set PR = p |-count (Radical n);
assume A1: p |^ 2 divides Radical n ; :: thesis: contradiction
A2: ( p <> 1 & Radical n <> 0 ) by INT_2:def 5;
A3: p |-count (Radical n) is non zero Element of NAT

proof

assume p |-count (Radical n) is not non zero Element of NAT ; :: thesis: contradiction
then ( p |^ 0 divides Radical n & not p |^ (0 + 1) divides Radical n ) by A2, NAT_3:def 7;
then not p divides Radical n by NEWTON:10;
hence contradiction by A1, Th10; :: thesis: verum

end;

p |-count (Radical n) >= 2

proof

assume p |-count (Radical n) < 2 ; :: thesis: contradiction
then p |-count (Radical n) = 1 by A3, NAT_1:23;
then not p |^ (1 + 1) divides Radical n by A2, NAT_3:def 7;
hence contradiction by A1; :: thesis: verum

end;

then p |-count (Radical n) > 1 by XXREAL_0:2;
hence contradiction by Th61; :: thesis: verum