let X be RealNormSpace; :: thesis: for V being Subset of X holds
( V is open iff for x being Point of X st x in V holds
ex r being Real st
( r > 0 & Ball (x,r) c= V ) )
let V be Subset of X; :: thesis: ( V is open iff for x being Point of X st x in V holds
ex r being Real st
( r > 0 & Ball (x,r) c= V ) )
reconsider V0 = V as Subset of (TopSpaceNorm X) ;

hereby :: thesis: ( ( for x being Point of X st x in V holds
ex r being Real st
( r > 0 & Ball (x,r) c= V ) ) implies V is open )

assume V is open ; :: thesis: for x being Point of X st x in V holds
ex r being Real st
( r > 0 & Ball (x,r) c= V )
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: verum

proof

let x be Point of X; :: thesis: ( x in V implies ex r being Real st
( r > 0 & Ball (x,r) c= V ) )
assume x in V ; :: thesis: ex r being Real st
( r > 0 & Ball (x,r) c= V )
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: ( r > 0 & Ball (x,r) c= V )
thus ( r > 0 & Ball (x,r) c= V ) by A2; :: thesis: verum

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: V is open
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: ( x in V0 implies ex r being Real st
( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V0 ) )
assume x in V0 ; :: thesis: ex r being Real st
( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V0 )
then consider r being Real such that
A4: ( r > 0 & Ball (x,r) c= V ) by A3;
take r ; :: thesis: ( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V0 )
thus ( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V0 ) by A4; :: thesis: verum

end;

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