theorem PsCompl: :: LATSTONE:28

for L being Lattice
for p being Prime
for x being Element of L st L = Divisors_Lattice (p * p) & x = p holds
x * = Bottom L