for V being RealNormSpace st not V is trivial holds
not DualSp V is trivial