theorem Th7: :: LATSTONE:9

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