theorem ThDE3: :: ZMODLAT3:33

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