theorem :: ZMODLAT2:38

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