let L be positive-definite RATional Z_Lattice; :: thesis: rank L = rank (DualLat L)
set I = the Basis of (EMLat L);
DualBasis the Basis of (EMLat L) is Basis of (DualLat L) by ThDLDB;
then rank (DualLat L) = card (DualBasis the Basis of (EMLat L)) by ZMODUL03:def 5
.= card the Basis of (EMLat L) by ThDB1
.= rank (EMLat L) by ZMODUL03:def 5 ;
hence rank L = rank (DualLat L) by ZMODLAT2:42; :: thesis: verum