for X being non trivial RealNormSpace ex w being VECTOR of X st ||.w.|| = 1