let L be Z_Lattice; :: thesis: for L1 being Z_Sublattice of L
for v being Vector of L
for w being Vector of L1 st w = v holds
- w = - v
let L1 be Z_Sublattice of L; :: thesis: for v being Vector of L
for w being Vector of L1 st w = v holds
- w = - v
let v be Vector of L; :: thesis: for w being Vector of L1 st w = v holds
- w = - v
let w be Vector of L1; :: thesis: ( w = v implies - w = - v )
assume AS: w = v ; :: thesis: - w = - v
L1 is Submodule of L by ThSL1;
hence - w = - v by AS, ZMODUL01:30; :: thesis: verum