:: deftheorem Def8 defines StoneSpace LOPCLSET:def 8 :
for BL being non trivial B_Lattice
for b₂ being strict TopSpace holds
( b₂ = StoneSpace BL iff ( the carrier of b₂ = ultraset BL & the topology of b₂ = { (union A) where A is Subset-Family of (ultraset BL) : A c= StoneR BL } ) );