for L being bounded pseudocomplemented Lattice
for x, y being Element of L st y is_a_pseudocomplement_of x holds
y in PseudoComplements x