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;

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 )

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

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

hence
V in the topology of (TOP-REAL n)
by A1, A2, PCOMPS_1:def 4; :: thesis: verum
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;( 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