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