let X be RealNormSpace; :: thesis: for V being Subset of () 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 (); :: 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 () & 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 () & V is open )
now :: thesis: for z being Element of () st z in V holds
ex r being Real st
( r > 0 & Ball (z,r) c= V )
let z be Element of (); :: 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 in the topology of () by PCOMPS_1:def 4; :: thesis: V is open
hence V is open ; :: 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 () ;
V in the topology of () by A4;
then consider r being Real such that
A6: ( r > 0 & Ball (z,r) c= V ) by ;
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