:: deftheorem defines Reflexive DUALSP02:def 4 :
for X being RealNormSpace holds
( X is Reflexive iff BidualFunc X is onto );