theorem ThELEM1: :: ZMODLAT3:36

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