:: deftheorem Def12 defines HTopSpace OPENLATT:def 12 :
for H being non trivial H_Lattice
for b₂ being strict TopStruct holds
( b₂ = HTopSpace H iff ( the carrier of b₂ = F_primeSet H & the topology of b₂ = { (union A) where A is Subset of (StoneS H) : verum } ) );