for V being RealLinearSpace
for W being Subspace of V holds
( Up W is Affine & 0. V in the carrier of W )