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 Th61
.= ( the Element of L `) "/\" the Element of L by Th34
.= Bottom L by Th61 ;
hence (Top L) ` = Bottom L ; :: thesis: verum