let H be non trivial H_Lattice; :: thesis: StoneH H preserves_top
(StoneH H) . (Top H) = F_primeSet H by Th28
.= the carrier of (HTopSpace H) by Def12
.= Top (Open_setLatt (HTopSpace H)) by Th9 ;
hence StoneH H preserves_top ; :: thesis: verum