for X being RealNormSpace holds
( X is Reflexive iff for f being Point of (DualSp (DualSp X)) ex x being Point of X st
for g being Point of (DualSp X) holds f . g = g . x )