theorem ThD: :: LATSTONE:6

for L being lower-bounded pseudocomplemented Lattice
for x being Element of L holds (x *) "/\" x = Bottom L