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