let L be lower-bounded pseudocomplemented Lattice; :: thesis: for a being Element of L holds a [= (a *) *
let a be Element of L; :: thesis: a [= (a *) *
a1: (a *) * is_a_pseudocomplement_of a * by def3;
a * is_a_pseudocomplement_of a by def3;
hence a [= (a *) * by a1; :: thesis: verum