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 ) )

ex r being Real st

( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V ) ) by A1; :: thesis: verum

( 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 :: 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 ) ) implies ( V in the topology of (TopSpaceNorm X) & V is open ) )

ex r being Real st

( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V ) ) implies ( V in the topology of (TopSpaceNorm X) & V is open ) )

assume A2:
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 )

hence V is open ; :: thesis: verum

end;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 :: thesis: for z being Element of (MetricSpaceNorm X) st z in V holds

ex r being Real st

( r > 0 & Ball (z,r) c= V )

hence
V in the topology of (TopSpaceNorm X)
by PCOMPS_1:def 4; :: thesis: V is open ex r being Real st

( r > 0 & Ball (z,r) c= V )

let z be Element of (MetricSpaceNorm X); :: thesis: ( z in V implies ex r being Real st

( r > 0 & Ball (z,r) c= V ) )

reconsider x = z as Point of X ;

assume z in V ; :: thesis: ex r being Real st

( r > 0 & Ball (z,r) c= V )

then consider r being Real such that

A3: ( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V ) by A2;

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 A3; :: thesis: verum

end;( r > 0 & Ball (z,r) c= V ) )

reconsider x = z as Point of X ;

assume z in V ; :: thesis: ex r being Real st

( r > 0 & Ball (z,r) c= V )

then consider r being Real such that

A3: ( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V ) by A2;

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 A3; :: thesis: verum

hence V is open ; :: thesis: verum

now :: thesis: ( V is open implies 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 ) )

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 ) )

assume A4:
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 )

end;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 A5: 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 A4;

then consider r being Real such that

A6: ( r > 0 & Ball (z,r) c= V ) by A5, PCOMPS_1:def 4;

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 A6; :: thesis: verum

end;( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V ) )

assume A5: 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 A4;

then consider r being Real such that

A6: ( r > 0 & Ball (z,r) c= V ) by A5, PCOMPS_1:def 4;

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 A6; :: thesis: verum

ex r being Real st

( r > 0 & { y where y is Point of X : ||.(x - y).|| < r } c= V ) ) by A1; :: thesis: verum