theorem ThDL1: :: ZMODLAT3:34

for L being positive-definite RATional Z_Lattice
for v being Vector of (DivisibleMod L) holds
( v in DualLat L iff v is Dual of L )