theorem ThDB1: :: ZMODLAT3:31

for L being positive-definite RATional Z_Lattice
for I being Basis of (EMLat L) holds card I = card (DualBasis I)