theorem Lm65A1: :: DUALSP02:6

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