:: deftheorem defines StoneS OPENLATT:def 7 :
for L being D_Lattice holds StoneS L = rng (StoneH L);