theorem Th23: :: OPENLATT:23

for L being D_Lattice holds LattStr(# (StoneS L),(Set_Union L),(Set_Meet L) #) is Lattice