let X be RealUnitarySpace; :: thesis: for V being Subset of (TopSpaceNorm (RUSp2RNSp 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 (RUSp2RNSp 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 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 is open

now :: thesis: for z being Element of (MetricSpaceNorm (RUSp2RNSp X)) st z in V holds
ex r being Real st
( r > 0 & Ball (z,r) c= V )

let z be Element of (MetricSpaceNorm (RUSp2RNSp 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;

hence V is open by PCOMPS_1:def 4; :: thesis: verum

end;

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

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 )

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 (RUSp2RNSp X)) ;
consider r being Real such that
A6: ( r > 0 & Ball (z,r) c= V ) by A5, A4, 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;

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