for X being RealNormSpace st not X is trivial holds
ex DuX being SubRealNormSpace of DualSp (DualSp X) ex L being Lipschitzian LinearOperator of X,DuX st
( L is bijective & DuX = Im (BidualFunc X) & ( for x being Point of X holds L . x = BiDual x ) & ( for x being Point of X holds ||.x.|| = ||.(L . x).|| ) )