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 () ;
A4: Z is open by ;
v in the carrier of X \ Y by ;
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 ;
consider w being VECTOR of X such that
A6: ( w in Y & ||.(v - w).|| <= e / 2 ) by A2, A5;
e / 2 < e by ;
then ||.(v - w).|| < e by ;
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