let L1 be Z_Sublattice of L; :: thesis: L1 is INTegral
thus for w1, w2 being Vector of L1 holds <;w1,w2;> in INT :: according to ZMODLAT1:def 5 :: thesis: verum

proof

let w1, w2 be Vector of L1; :: thesis: <;w1,w2;> in INT
reconsider v1 = w1, v2 = w2 as Vector of L by ThSL4;
<;w1,w2;> = <;v1,v2;> by ThSL18;
hence <;w1,w2;> in INT by defIntegral; :: thesis: verum

end;