p is square-free by MOEBIUS1:23;
hence Divisors_Lattice p is Boolean ; :: thesis: verum