theorem Th13: :: OPENLATT:13

for L being D_Lattice
for x being set holds
( x in StoneS L iff ex a being Element of L st x = (StoneH L) . a )