let X be strict RealNormSpace; :: thesis:
let A be non empty Subset of X; :: thesis:
assume A0: for f being Point of (DualSp X) st ( for x being Point of X st x in A holds
(Bound2Lipschitz (f,X)) . x = 0 ) holds
Bound2Lipschitz (f,X) = 0. (DualSp X) ; :: thesis:
set M = ClNLin A;
consider Z being Subset of X such that
Q0: ( Z = the carrier of (Lin A) & ClNLin A = NORMSTR(# (Cl Z),(Zero_ ((Cl Z),X)),(Add_ ((Cl Z),X)),(Mult_ ((Cl Z),X)),(Norm_ ((Cl Z),X)) #) ) by NORMSP_3:def 20;
reconsider Y = the carrier of (ClNLin A) as non empty Subset of X by DUALSP01:def 16;
Q23: Y is linearly-closed by NORMSP_3:29;
Y = the carrier of X

assume Y <> the carrier of X ; :: thesis:
then not the carrier of X c= Y ;
then consider x0 being object such that
Q25: ( x0 in the carrier of X & not x0 in Y ) ;
reconsider x0 = x0 as Point of X by Q25;
consider G being Point of (DualSp X) such that
Q26: for x being Point of X st x in Y holds
(Bound2Lipschitz (G,X)) . x = 0 and
Q27: (Bound2Lipschitz (G,X)) . x0 = 1 by Q0, Q23, Q25, DUALSP02:2;
for x being Point of X st x in A holds
(Bound2Lipschitz (G,X)) . x = 0

end;

then (Bound2Lipschitz (G,X)) . x0 = (0. (DualSp X)) . x0 by A0
.= ( the carrier of X --> 0) . x0 by DUALSP01:25
.= 0 ;
hence contradiction by Q27; :: thesis:

end;