let BL be Boolean Lattice; :: thesis: (Top BL) ` = Bottom BL
set a = Bottom BL;
thus (Top BL) ` = ((Bottom BL) "\/" ((Bottom BL) `)) ` by LATTICES:21
.= ((Bottom BL) `) "/\" (((Bottom BL) `) `)
.= Bottom BL ; :: thesis: verum