let X be RealNormSpace; :: thesis: for Y being Subset of X

for v being VECTOR of X st Y is closed & ( for e being Real st 0 < e holds

ex w being VECTOR of X st

( w in Y & ||.(v - w).|| <= e ) ) holds

v in Y

let Y be Subset of X; :: thesis: for v being VECTOR of X st Y is closed & ( for e being Real st 0 < e holds

ex w being VECTOR of X st

( w in Y & ||.(v - w).|| <= e ) ) holds

v in Y

let v be VECTOR of X; :: thesis: ( Y is closed & ( for e being Real st 0 < e holds

ex w being VECTOR of X st

( w in Y & ||.(v - w).|| <= e ) ) implies v in Y )

assume that

A1: Y is closed and

A2: for e being Real st 0 < e holds

ex w being VECTOR of X st

( w in Y & ||.(v - w).|| <= e ) ; :: thesis: v in Y

assume A3: not v in Y ; :: thesis: contradiction

reconsider Z = Y ` as Subset of (TopSpaceNorm X) ;

A4: Z is open by A1, NORMSP_2:16;

v in the carrier of X \ Y by A3, XBOOLE_0:def 5;

then v in Z by SUBSET_1:def 4;

then consider e being Real such that

A5: ( e > 0 & { y where y is Point of X : ||.(v - y).|| < e } c= Z ) by A4, NORMSP_2:7;

consider w being VECTOR of X such that

A6: ( w in Y & ||.(v - w).|| <= e / 2 ) by A2, A5;

e / 2 < e by A5, XREAL_1:216;

then ||.(v - w).|| < e by A6, XXREAL_0:2;

then w in { y where y is Point of X : ||.(v - y).|| < e } ;

then w in Y ` by A5;

then w in the carrier of X \ Y by SUBSET_1:def 4;

hence contradiction by A6, XBOOLE_0:def 5; :: thesis: verum

for v being VECTOR of X st Y is closed & ( for e being Real st 0 < e holds

ex w being VECTOR of X st

( w in Y & ||.(v - w).|| <= e ) ) holds

v in Y

let Y be Subset of X; :: thesis: for v being VECTOR of X st Y is closed & ( for e being Real st 0 < e holds

ex w being VECTOR of X st

( w in Y & ||.(v - w).|| <= e ) ) holds

v in Y

let v be VECTOR of X; :: thesis: ( Y is closed & ( for e being Real st 0 < e holds

ex w being VECTOR of X st

( w in Y & ||.(v - w).|| <= e ) ) implies v in Y )

assume that

A1: Y is closed and

A2: for e being Real st 0 < e holds

ex w being VECTOR of X st

( w in Y & ||.(v - w).|| <= e ) ; :: thesis: v in Y

assume A3: not v in Y ; :: thesis: contradiction

reconsider Z = Y ` as Subset of (TopSpaceNorm X) ;

A4: Z is open by A1, NORMSP_2:16;

v in the carrier of X \ Y by A3, XBOOLE_0:def 5;

then v in Z by SUBSET_1:def 4;

then consider e being Real such that

A5: ( e > 0 & { y where y is Point of X : ||.(v - y).|| < e } c= Z ) by A4, NORMSP_2:7;

consider w being VECTOR of X such that

A6: ( w in Y & ||.(v - w).|| <= e / 2 ) by A2, A5;

e / 2 < e by A5, XREAL_1:216;

then ||.(v - w).|| < e by A6, XXREAL_0:2;

then w in { y where y is Point of X : ||.(v - y).|| < e } ;

then w in Y ` by A5;

then w in the carrier of X \ Y by SUBSET_1:def 4;

hence contradiction by A6, XBOOLE_0:def 5; :: thesis: verum