let L be distributive bounded well-complemented preOrthoLattice; :: thesis: (Top L) ` = Bottom L
consider x being Element of L;
(Top L) ` = (((x ` ) ` ) + (x ` )) ` by Th61
.= (x ` ) "/\" x by Th34
.= Bottom L by Th61 ;
hence (Top L) ` = Bottom L ; :: thesis: verum