let L be lower-bounded pseudocomplemented Lattice; :: thesis: for x being Element of L holds (x *) "/\" x = Bottom L
let x be Element of L; :: thesis: (x *) "/\" x = Bottom L
x * is_a_pseudocomplement_of x by def3;
hence (x *) "/\" x = Bottom L ; :: thesis: verum