theorem Th28: :: CLVECT_1:28

for V being ComplexLinearSpace
for W being Subspace of V
for x being object st x in W holds
x in V