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