:: deftheorem defines StoneR LATTICEA:def 6 :
for L being distributive Lattice holds StoneR L = rng (PrimeFilters L);