theorem Th11: :: VECTSP10:11

for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr
for V being VectSp of K
for V1 being Subspace of V
for W1 being Subspace of V1
for v being Vector of V st v in W1 holds
v is Vector of V1