let H be non trivial H_Lattice; :: thesis: StoneH H preserves_bottom
(StoneH H) . (Bottom H) = {} by Th29
.= Bottom (Open_setLatt (HTopSpace H)) by Th8 ;
hence StoneH H preserves_bottom ; :: thesis: verum