let n be Nat; :: thesis: ( n is square-free implies for p being Prime holds p |-count n <= 1 )
assume A1: n is square-free ; :: 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; :: thesis: verum