theorem ThRatLat1A: :: ZMODLAT3:47

for L being Z_Lattice
for I being Basis of L st ( for v, u being Vector of L st v in I & u in I holds
<;v,u;> in RAT ) holds
for v, u being Vector of L holds <;v,u;> in RAT