theorem :: DUALSP02:22

for X being RealNormSpace holds
( X is Reflexive iff Im (BidualFunc X) = DualSp (DualSp X) )