:: deftheorem FG defines FreeGen MOEBIUS2:def 5 :
for p being Prime
for b₂ being Subset of NAT holds
( b₂ = FreeGen p iff for n being Nat holds
( n in b₂ iff ( n is square-free & ( for i being Prime st i divides n holds
i <= p ) ) ) );