theorem :: ZMODLAT3:29

for L being Z_Lattice holds DualLatMod L is Submodule of DivisibleMod L