let L be bounded pseudocomplemented Lattice; :: thesis: for x being Element of L holds x * in PseudoComplements x
let a be Element of L; :: thesis: a * in PseudoComplements a
a * is_a_pseudocomplement_of a by def3;
hence a * in PseudoComplements a by ThF; :: thesis: verum