let X be RealNormSpace; :: thesis: for V being Subset of (TopSpaceNorm X) holds
( V is open iff for x being Point of X st x in V holds
ex r being Real st
( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V ) )
let V be Subset of (TopSpaceNorm X); :: thesis: ( V is open iff for x being Point of X st x in V holds
ex r being Real st
( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V ) )

A1: now

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

hereby :: thesis: verum

let x be Point of X; :: thesis: ( x in V implies ex r being Real st
( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V ) )
assume A3: x in V ; :: thesis: ex r being Real st
( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V )
reconsider z = x as Element of (MetricSpaceNorm X) ;
V in the topology of (TopSpaceNorm X) by A2, PRE_TOPC:def 5;
then consider r being Real such that
A4: ( r > 0 & Ball z,r c= V ) by A3, PCOMPS_1:def 5;
take r = r; :: thesis: ( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V )
ex t being Point of X st
( t = z & Ball z,r = { y where y is Point of X : ||.(t - y).|| < r } ) by Th2;
hence ( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V ) by A4; :: thesis: verum

end;

end;

now

assume A5: for x being Point of X st x in V holds
ex r being Real st
( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V ) ; :: thesis: ( V in the topology of (TopSpaceNorm X) & V is open )

now

let z be Element of (MetricSpaceNorm X); :: thesis: ( z in V implies ex r being Real st
( r > 0 & Ball z,r c= V ) )
assume A6: z in V ; :: thesis: ex r being Real st
( r > 0 & Ball z,r c= V )
reconsider x = z as Point of X ;
consider r being Real such that
A7: ( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V ) by A5, A6;
take r = r; :: thesis: ( r > 0 & Ball z,r c= V )
ex t being Point of X st
( t = z & Ball z,r = { y where y is Point of X : ||.(t - y).|| < r } ) by Th2;
hence ( r > 0 & Ball z,r c= V ) by A7; :: thesis: verum

end;

hence V in the topology of (TopSpaceNorm X) by PCOMPS_1:def 5; :: thesis: V is open
hence V is open by PRE_TOPC:def 5; :: thesis: verum

end;

hence ( V is open iff for x being Point of X st x in V holds
ex r being Real st
( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V ) ) by A1; :: thesis: verum