theorem :: ZMODLAT3:44

for L being INTegral positive-definite Z_Lattice holds EMLat L is Z_Sublattice of DualLat L