let L be Z_Lattice; :: thesis: for b being OrdBasis of L st GramMatrix ((),b) is Matrix of dim L,INT.Ring holds
L is INTegral

let b be OrdBasis of L; :: thesis: ( GramMatrix ((),b) is Matrix of dim L,INT.Ring implies L is INTegral )
assume A1: GramMatrix ((),b) is Matrix of dim L,INT.Ring ; :: thesis: L is INTegral
set I = rng b;
reconsider I = rng b as Basis of L by ZMATRLIN:def 5;
set GM = GramMatrix ((),b);
reconsider GMI = GramMatrix ((),b) as Matrix of dim L,INT.Ring by A1;
for v, u being Vector of L st v in I & u in I holds
<;v,u;> in INT
proof
let v, u be Vector of L; :: thesis: ( v in I & u in I implies <;v,u;> in INT )
assume B1: ( v in I & u in I ) ; :: thesis: <;v,u;> in INT
consider i being Nat such that
B2: ( i in dom b & b . i = v ) by ;
consider j being Nat such that
B3: ( j in dom b & b . j = u ) by ;
B4: b /. i = v by ;
B6: (GramMatrix ((),b)) * (i,j) = () . ((b /. i),(b /. j)) by
.= <;v,u;> by ;
B7: dom b = Seg (len b) by FINSEQ_1:def 3
.= Seg (dim L) by ZMATRLIN:49 ;
Indices (GramMatrix ((),b)) = [:(Seg (dim L)),(Seg (dim L)):] by MATRIX_0:24;
then [i,j] in Indices (GramMatrix ((),b)) by ;
then (GramMatrix ((),b)) * (i,j) = GMI * (i,j) by ZMATRLIN:1;
hence <;v,u;> in INT by B6; :: thesis: verum
end;
hence L is INTegral by ZMODLAT1:15; :: thesis: verum