theorem Th2: :: LATSTONE:5

for L being lower-bounded pseudocomplemented Lattice
for a, b, x being Element of L st a is_a_pseudocomplement_of x & b is_a_pseudocomplement_of x holds
a = b