theorem LmEMDetX8: :: ZMODLAT2:39

for L being Z_Lattice
for b being FinSequence of L holds
( b is OrdBasis of L iff (MorphsZQ L) * b is OrdBasis of EMbedding L )