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 *) *) * [= a * by Th6, Th5;
a * [= ((a *) *) * by Th5;
hence a * = ((a *) *) * by a1, LATTICES:8; :: thesis: verum