let L be Lattice; :: thesis: for p being Prime
for x being Element of L st L = Divisors_Lattice (p * p) & x = p holds
x * = Bottom L
let p be Prime; :: thesis: for x being Element of L st L = Divisors_Lattice (p * p) & x = p holds
x * = Bottom L
let x be Element of L; :: thesis: ( L = Divisors_Lattice (p * p) & x = p implies x * = Bottom L )
assume that
A1: L = Divisors_Lattice (p * p) and
B0: x = p ; :: thesis: x * = Bottom L
reconsider pp = Bottom L as Element of L ;
for y being Element of L st x "/\" y = Bottom L holds
y [= pp

proof

let y be Element of L; :: thesis: ( x "/\" y = Bottom L implies y [= pp )
y in the carrier of L ;
then y in NatDivisors (p * p) by A1, MOEBIUS2:def 10;
then y in {1,p,(p * p)} by DivisorsSquare;
then w3: ( y = 1 or y = p or y = p * p ) by ENUMSET1:def 1;
assume W1: x "/\" y = Bottom L ; :: thesis: y [= pp
W2: y <> Top L

proof

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

end;

y <> p

proof

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

end;

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

end;

then pp is_a_pseudocomplement_of x by A1;
hence x * = Bottom L by def3, A1; :: thesis: verum