let n be Nat; :: thesis: ( n <> 0 & ( for p being Prime holds p |-count n <= 1 ) implies n is square-free )
assume A1: ( n <> 0 & ( for p being Prime holds p |-count n <= 1 ) ) ; :: thesis: n is square-free
assume n is square-containing ; :: thesis: contradiction
then consider p being Prime such that
A2: p |^ 2 divides n by MOEBIUS1:def 1;
p |-count n >= 1 + 1 by A1, A2, Ciek;
hence contradiction by A1, NAT_1:13; :: thesis: verum