theorem LmEMDetX6: :: ZMODLAT2:37

for L being Z_Lattice
for I being Subset of L holds
( I is Basis of L iff (MorphsZQ L) .: I is Basis of (EMbedding L) )