theorem Th5: :: LATSTONE:7

for L being lower-bounded pseudocomplemented Lattice
for a being Element of L holds a [= (a *) *