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