theorem :: ZMODLAT3:40

for L being positive-definite RATional Z_Lattice
for b being OrdBasis of EMLat L
for I being Basis of (EMLat L) st I = rng b holds
(B2DB I) * b is OrdBasis of DualLat L