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) `) `) by LATTICES:24
.= Bottom BL by LATTICES:20 ; :: thesis: verum