let n be natural number ; :: thesis: ( not n is square-containing implies for p being Prime holds p |-count n <= 1 )
assume A1: not n is square-containing ; :: thesis: for p being Prime holds p |-count n <= 1
given p being Prime such that A2: p |-count n > 1 ; :: thesis: contradiction
p |-count n >= 1 + 1 by A2, NAT_1:13;
then p |^ 2 divides n by A1, Th9, Th21;
hence contradiction by A1, Def1; :: thesis: verum