let L be bounded pseudocomplemented Lattice; :: thesis: for x, y being Element of L st y is_a_pseudocomplement_of x holds
y in PseudoComplements x
let x, y be Element of L; :: thesis: ( y is_a_pseudocomplement_of x implies y in PseudoComplements x )
assume y is_a_pseudocomplement_of x ; :: thesis: y in PseudoComplements x
then x "/\" y = Bottom L ;
then y in { xx where xx is Element of L : x "/\" xx = Bottom L } ;
hence y in PseudoComplements x by LATTICEA:def 8; :: thesis: verum