let H be non trivial H_Lattice; :: thesis: StoneH H preserves_top
(StoneH H) . (Top H) = F_primeSet H by Th33
.= the carrier of (HTopSpace H) by Def12
.= Top (Open_setLatt (HTopSpace H)) by Th11 ;
hence StoneH H preserves_top by LATTICE4:def 4; :: thesis: verum