let L be D_Lattice; :: thesis: StoneH L is bijective
thus StoneH L is one-to-one by Th25; :: according to FUNCT_2:def 4 :: thesis: StoneH L is onto
thus rng (StoneH L) = the carrier of (StoneLatt L) ; :: according to FUNCT_2:def 3 :: thesis: verum