:: deftheorem Def6 defines StoneH OPENLATT:def 6 :
for L being D_Lattice
for b₂ being Function holds
( b₂ = StoneH L iff for a being Element of L holds
( dom b₂ = the carrier of L & b₂ . a = { F where F is Filter of L : ( F in F_primeSet L & a in F ) } ) );