theorem Th6: :: LATSTONE:8

for L being lower-bounded pseudocomplemented Lattice
for a, b being Element of L st a [= b holds
b * [= a *