let L be bounded pseudocomplemented Lattice; :: thesis: (Bottom L) * = Top L
Top L is_a_pseudocomplement_of Bottom L by LATTICES:19;
hence (Bottom L) * = Top L by def3; :: thesis: verum