for V being RealUnitarySpace
for v being VECTOR of V ex W being Subspace of V st the carrier of W = { u where u is VECTOR of V : u .|. v = 0 }