theorem LmDE0: :: ZMODLAT3:26
for L being Z_Lattice holds 0. (DivisibleMod L) is Dual of L