let L be Z_Lattice; :: thesis: for L1 being Z_Sublattice of L
for v1, v2 being Vector of L st v1 in L1 & v2 in L1 holds
v1 - v2 in L1
let L1 be Z_Sublattice of L; :: thesis: for v1, v2 being Vector of L st v1 in L1 & v2 in L1 holds
v1 - v2 in L1
let v1, v2 be Vector of L; :: thesis: ( v1 in L1 & v2 in L1 implies v1 - v2 in L1 )
assume AS: ( v1 in L1 & v2 in L1 ) ; :: thesis: v1 - v2 in L1
L1 is Submodule of L by ThSL1;
hence v1 - v2 in L1 by AS, ZMODUL01:39; :: thesis: verum