theorem :: ZMODLAT3:37

for L being Z_Lattice
for I being Basis of (EMbedding L) holds I is Basis of (EMLat L)