set L = Divisors_Lattice (p * p);
the carrier of (Divisors_Lattice (p * p)) = NatDivisors (p * p) by MOEBIUS2:def 10;
then A1: the carrier of (Divisors_Lattice (p * p)) = {1,p,(p * p)} by DivisorsSquare;
for x being Element of (Divisors_Lattice (p * p)) ex y being Element of (Divisors_Lattice (p * p)) st y is_a_pseudocomplement_of x

proof

let x be Element of (Divisors_Lattice (p * p)); :: thesis: ex y being Element of (Divisors_Lattice (p * p)) st y is_a_pseudocomplement_of x

per cases ( x = 1 or x = p or x = p * p ) by ENUMSET1:def 1, A1;

suppose C1: x = 1 ; :: thesis: ex y being Element of (Divisors_Lattice (p * p)) st y is_a_pseudocomplement_of x

reconsider pp = p * p as Element of (Divisors_Lattice (p * p)) by A1, ENUMSET1:def 1;
x = Bottom (Divisors_Lattice (p * p)) by C1, MOEBIUS2:64;
then B1: pp "/\" x = Bottom (Divisors_Lattice (p * p)) ;
for y being Element of (Divisors_Lattice (p * p)) st x "/\" y = Bottom (Divisors_Lattice (p * p)) holds
y [= pp

proof

let y be Element of (Divisors_Lattice (p * p)); :: thesis: ( x "/\" y = Bottom (Divisors_Lattice (p * p)) implies y [= pp )
assume x "/\" y = Bottom (Divisors_Lattice (p * p)) ; :: thesis: y [= pp
pp = Top (Divisors_Lattice (p * p)) by MOEBIUS2:64;
hence y [= pp by LATTICES:19; :: thesis: verum

end;

then pp is_a_pseudocomplement_of x by B1;
hence ex y being Element of (Divisors_Lattice (p * p)) st y is_a_pseudocomplement_of x ; :: thesis: verum

end;

suppose B0: x = p ; :: thesis: ex y being Element of (Divisors_Lattice (p * p)) st y is_a_pseudocomplement_of x

reconsider pp = Bottom (Divisors_Lattice (p * p)) as Element of (Divisors_Lattice (p * p)) ;
for y being Element of (Divisors_Lattice (p * p)) st x "/\" y = Bottom (Divisors_Lattice (p * p)) holds
y [= pp

proof

let y be Element of (Divisors_Lattice (p * p)); :: thesis: ( x "/\" y = Bottom (Divisors_Lattice (p * p)) implies y [= pp )
w3: ( y = 1 or y = p or y = p * p ) by A1, ENUMSET1:def 1;
assume W1: x "/\" y = Bottom (Divisors_Lattice (p * p)) ; :: thesis: y [= pp
W2: y <> Top (Divisors_Lattice (p * p))

proof

assume y = Top (Divisors_Lattice (p * p)) ; :: thesis: contradiction
then p = 1 by B0, MOEBIUS2:64, W1;
hence contradiction by INT_2:def 4; :: thesis: verum

end;

y <> p

proof

assume y = p ; :: thesis: contradiction
then 1 = p by W1, MOEBIUS2:64, B0;
hence contradiction by INT_2:def 4; :: thesis: verum

end;

hence y [= pp by W2, w3, MOEBIUS2:64; :: thesis: verum

end;

then pp is_a_pseudocomplement_of x ;
hence ex y being Element of (Divisors_Lattice (p * p)) st y is_a_pseudocomplement_of x ; :: thesis: verum

end;

suppose C1: x = p * p ; :: thesis: ex y being Element of (Divisors_Lattice (p * p)) st y is_a_pseudocomplement_of x

reconsider pp = 1 as Element of (Divisors_Lattice (p * p)) by A1, ENUMSET1:def 1;
b1: pp = Bottom (Divisors_Lattice (p * p)) by MOEBIUS2:64;
for y being Element of (Divisors_Lattice (p * p)) st x "/\" y = Bottom (Divisors_Lattice (p * p)) holds
y [= pp

proof

let y be Element of (Divisors_Lattice (p * p)); :: thesis: ( x "/\" y = Bottom (Divisors_Lattice (p * p)) implies y [= pp )
assume S1: x "/\" y = Bottom (Divisors_Lattice (p * p)) ; :: thesis: y [= pp
s3: ( y = 1 or y = p * p or y = p ) by A1, ENUMSET1:def 1;
R2: Top (Divisors_Lattice (p * p)) = p * p by MOEBIUS2:64;
y <> p

proof

assume y = p ; :: thesis: contradiction
then p = 1 by MOEBIUS2:64, S1, R2, C1;
hence contradiction by INT_2:def 4; :: thesis: verum

end;

hence y [= pp by s3, C1, MOEBIUS2:64, S1; :: thesis: verum

end;

then pp is_a_pseudocomplement_of x by b1;
hence ex y being Element of (Divisors_Lattice (p * p)) st y is_a_pseudocomplement_of x ; :: thesis: verum

end;

end;

end;

hence Divisors_Lattice (p * p) is pseudocomplemented ; :: thesis: verum