let L be D_Lattice; :: thesis: StoneLatt L is distributive
StoneH L is onto by FUNCT_2:def 3;
hence StoneLatt L is distributive by LATTICE4:18; :: thesis: verum