theorem Th39: :: ZMODUL01:39

for V being Z_Module
for u, v being Vector of V
for W being Submodule of V st u in W & v in W holds
u - v in W by VECTSP_4:23;