let L be distributive bounded well-complemented preOrthoLattice; :: thesis: (Top L) ` = Bottom L
set x = the Element of L;
(Top L) ` = ((( the Element of L `) `) + ( the Element of L `)) ` by Th59
.= ( the Element of L `) "/\" the Element of L by Th33
.= Bottom L by Th59 ;
hence (Top L) ` = Bottom L ; :: thesis: verum