let L be positive-definite RATional Z_Lattice; :: thesis: for I being Basis of (EMLat L) holds card I = card (DualBasis I)
let I be Basis of (EMLat L); :: thesis: card I = card (DualBasis I)
( B2DB I is one-to-one & dom (B2DB I) = I & rng (B2DB I) = DualBasis I ) by defB2DB;
hence card I = card (DualBasis I) by CARD_1:5, WELLORD2:def 4; :: thesis: verum