for n being Nat st n <> 0 & ( for p being Prime holds p |-count n <= 1 ) holds
n is square-free