:: deftheorem defines Up RUSUB_4:def 6 :
for V being RealUnitarySpace
for W being Subspace of V holds Up W = the carrier of W;