theorem :: MOEBIUS2:65

for n being non zero Nat holds
( Divisors_Lattice n is Boolean iff n is square-free )