p |^ 2 divides p * p by NEWTON:81;
then p * p is square-containing by MOEBIUS1:def 1;
hence ( not Divisors_Lattice (p * p) is Boolean & Divisors_Lattice (p * p) is Stone ) by MOEBIUS2:65; :: thesis: verum