:: deftheorem defines Up CONVEX4:def 19 :
for V being ComplexLinearSpace
for W being Subspace of V holds Up W = the carrier of W;