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

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