let X be RealNormSpace; :: thesis:
let V be Subset of X; :: thesis:
reconsider V0 = V as Subset of (TopSpaceNorm X) ;

hereby :: thesis:

assume V is open ; :: thesis:
then A1: V0 is open by NORMSP_2:16;
thus for x being Point of X st x in V holds
ex r being Real st
( r > 0 & Ball (x,r) c= V ) :: thesis:

proof

let x be Point of X; :: thesis:
assume x in V ; :: thesis:
then consider r being Real such that
A2: ( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V0 ) by A1, NORMSP_2:7;
take r ; :: thesis:
thus ( r > 0 & Ball (x,r) c= V ) by A2; :: thesis:

end;

end;

assume A3: for x being Point of X st x in V holds
ex r being Real st
( r > 0 & Ball (x,r) c= V ) ; :: thesis:
for x being Point of X st x in V0 holds
ex r being Real st
( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V0 )

proof

let x be Point of X; :: thesis:
assume x in V0 ; :: thesis:
then consider r being Real such that
A4: ( r > 0 & Ball (x,r) c= V ) by A3;
take r ; :: thesis:
thus ( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V0 ) by A4; :: thesis:

end;

then V0 is open by NORMSP_2:7;
hence V is open by NORMSP_2:16; :: thesis: