:: deftheorem defines square-containing MOEBIUS1:def 1 :
for x being Nat holds
( x is square-containing iff ex p being Prime st p |^ 2 divides x );