theorem ThDivisibleL1: :: ZMODLAT2:20

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