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