theorem ThDivisibleL2: :: ZMODLAT2:21

for L being Z_Lattice
for r being Element of F_Rat holds EMLat (r,L) is Submodule of DivisibleMod L