theorem LmDE0: :: ZMODLAT3:26

for L being Z_Lattice holds 0. (DivisibleMod L) is Dual of L