let L be RATional Z_Lattice; :: thesis: for b being OrdBasis of L holds Det (GramMatrix b) in F_Rat
let b be OrdBasis of L; :: thesis: Det (GramMatrix b) in F_Rat
GramMatrix b is Matrix of dim L,F_Rat by ThGM1;
hence Det (GramMatrix b) in F_Rat by LmGM11; :: thesis: verum