theorem CLOSE1: :: NORMSP_3:25

for X being RealNormSpace
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