:: deftheorem Def1 defines BiDual DUALSP02:def 1 :
for X being RealNormSpace
for x being Point of X
for b₃ being Point of (DualSp (DualSp X)) holds
( b₃ = BiDual x iff for f being Point of (DualSp X) holds b₃ . f = f . x );