:: deftheorem StoneDef defines StoneSpace LATTICEA:def 7 :
for L being distributive upper-bounded Lattice
for b₂ being strict TopSpace holds
( b₂ = StoneSpace L iff ( the carrier of b₂ = PFilters L & the topology of b₂ = { (union A) where A is Subset-Family of (PFilters L) : A c= StoneR L } ) );