theorem ThDLDB: :: ZMODLAT3:39

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