let L be non trivial positive-definite RATional Z_Lattice; :: thesis: for b being OrdBasis of L holds (GramMatrix b) ~ is Matrix of dim L,F_Rat
let b be OrdBasis of L; :: thesis: (GramMatrix b) ~ is Matrix of dim L,F_Rat
GramMatrix b is Matrix of dim L,F_Rat by ZMODLAT2:45;
hence (GramMatrix b) ~ is Matrix of dim L,F_Rat by INVMN2; :: thesis: verum