:: deftheorem Def2 defines SCNAT MOEBIUS1:def 2 :
for b₁ being Subset of NAT holds
( b₁ = SCNAT iff for n being Nat holds
( n in b₁ iff n is square-free ) );