set p = the Prime;
take Divisors_Lattice ( the Prime * the Prime) ; :: thesis: ( Divisors_Lattice ( the Prime * the Prime) is Stone & not Divisors_Lattice ( the Prime * the Prime) is Boolean )
thus ( Divisors_Lattice ( the Prime * the Prime) is Stone & not Divisors_Lattice ( the Prime * the Prime) is Boolean ) ; :: thesis: verum