let L be Z_Lattice; :: thesis: for L1 being Z_Sublattice of L
for w being Vector of L1 holds w is Vector of L
let L1 be Z_Sublattice of L; :: thesis: for w being Vector of L1 holds w is Vector of L
let w be Vector of L1; :: thesis: w is Vector of L
L1 is Submodule of L by ThSL1;
hence w is Vector of L by ZMODUL01:25; :: thesis: verum