theorem ThDB2: :: ZMODLAT3:38

for L being positive-definite RATional Z_Lattice
for I being Basis of (EMLat L)
for v being Vector of (DivisibleMod L) st v in DualBasis I holds
v is Dual of L