set L = Divisors_Lattice (p * p);
let x be Element of (Divisors_Lattice (p * p)); :: according to LATSTONE:def 5 :: thesis: (x *) "\/" ((x *) *) = Top (Divisors_Lattice (p * p))
x in the carrier of (Divisors_Lattice (p * p)) ;
then x in NatDivisors (p * p) by MOEBIUS2:def 10;
then x in {1,p,(p * p)} by DivisorsSquare;

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

suppose x = 1 ; :: thesis: (x *) "\/" ((x *) *) = Top (Divisors_Lattice (p * p))

then x = Bottom (Divisors_Lattice (p * p)) by MOEBIUS2:64;
then x * = Top (Divisors_Lattice (p * p)) by Th11;
hence (x *) "\/" ((x *) *) = Top (Divisors_Lattice (p * p)) ; :: thesis: verum

end;

suppose x = p ; :: thesis: (x *) "\/" ((x *) *) = Top (Divisors_Lattice (p * p))

then x * = Bottom (Divisors_Lattice (p * p)) by PsCompl;
hence (x *) "\/" ((x *) *) = Top (Divisors_Lattice (p * p)) by Th11; :: thesis: verum

end;

suppose x = p * p ; :: thesis: (x *) "\/" ((x *) *) = Top (Divisors_Lattice (p * p))

then x = Top (Divisors_Lattice (p * p)) by MOEBIUS2:64;
then x * = Bottom (Divisors_Lattice (p * p)) by Th11a;
hence (x *) "\/" ((x *) *) = Top (Divisors_Lattice (p * p)) by Th11; :: thesis: verum

end;

end;