let n be Nat; :: thesis: for V being Subset of (TOP-REAL n) holds
( V in the topology of (TOP-REAL n) iff for p being Point of (TOP-REAL n) st p in V holds
ex r being Real st
( r > 0 & Ball (p,r) c= V ) )
let V be Subset of (TOP-REAL n); :: thesis: ( V in the topology of (TOP-REAL n) iff for p being Point of (TOP-REAL n) st p in V holds
ex r being Real st
( r > 0 & Ball (p,r) c= V ) )
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
set T = TOP-REAL n;
A1: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
A2: TopSpaceMetr (Euclid n) = TopStruct(# the carrier of (Euclid n),(Family_open_set (Euclid n)) #) by PCOMPS_1:def 5;
reconsider V1 = V as Subset of (Euclid n) by EUCLID:67;

hereby :: thesis: ( ( for p being Point of (TOP-REAL n) st p in V holds
ex r being Real st
( r > 0 & Ball (p,r) c= V ) ) implies V in the topology of (TOP-REAL n) )

assume A3: V in the topology of (TOP-REAL n) ; :: thesis: for p being Point of (TOP-REAL n) st p in V holds
ex r being Real st
( r > 0 & Ball (p,r) c= V )
let p be Point of (TOP-REAL n); :: thesis: ( p in V implies ex r being Real st
( r > 0 & Ball (p,r) c= V ) )
assume A4: p in V ; :: thesis: ex r being Real st
( r > 0 & Ball (p,r) c= V )
reconsider x = p as Element of (Euclid n) by EUCLID:67;
consider r being Real such that
A5: ( r > 0 & Ball (x,r) c= V1 ) by A3, A4, A1, A2, PCOMPS_1:def 4;
reconsider r = r as Real ;
take r = r; :: thesis: ( r > 0 & Ball (p,r) c= V )
thus r > 0 by A5; :: thesis: Ball (p,r) c= V
reconsider x1 = x as Point of (Euclid n1) ;
reconsider p1 = p as Point of (TOP-REAL n1) ;
thus Ball (p,r) c= V by A5, TOPREAL9:13; :: thesis: verum

end;

assume A6: for p being Point of (TOP-REAL n) st p in V holds
ex r being Real st
( r > 0 & Ball (p,r) c= V ) ; :: thesis: V in the topology of (TOP-REAL n)
for x being Element of (Euclid n) st x in V1 holds
ex r being Real st
( r > 0 & Ball (x,r) c= V1 )

proof

let x be Element of (Euclid n); :: thesis: ( x in V1 implies ex r being Real st
( r > 0 & Ball (x,r) c= V1 ) )
assume A7: x in V1 ; :: thesis: ex r being Real st
( r > 0 & Ball (x,r) c= V1 )
reconsider p = x as Point of (TOP-REAL n) by EUCLID:67;
consider r being Real such that
A8: ( r > 0 & Ball (p,r) c= V ) by A6, A7;
take r ; :: thesis: ( r > 0 & Ball (x,r) c= V1 )
thus r > 0 by A8; :: thesis: Ball (x,r) c= V1
reconsider x1 = x as Point of (Euclid n1) ;
reconsider p1 = p as Point of (TOP-REAL n1) ;
thus Ball (x,r) c= V1 by A8, TOPREAL9:13; :: thesis: verum

end;

hence V in the topology of (TOP-REAL n) by A1, A2, PCOMPS_1:def 4; :: thesis: verum