theorem :: OPENLATT:24

for L being D_Lattice holds the carrier of (StoneLatt L) = StoneS L ;