let H be non trivial H_Lattice; :: thesis: StoneH H preserves_bottom
(StoneH H) . (Bottom H) = {} by Th34
.= Bottom (Open_setLatt (HTopSpace H)) by Th10 ;
hence StoneH H preserves_bottom by LATTICE4:def 8; :: thesis: verum