let L be D_Lattice; :: thesis: L, StoneLatt L are_isomorphic
take StoneH L ; :: according to LATTICE4:def 3 :: thesis: StoneH L is bijective
thus StoneH L is bijective ; :: thesis: verum