let n be Nat; 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); ( 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 ( ( 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)
;
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);
( p in V implies ex r being Real st
( r > 0 & Ball (p,r) c= V ) )assume A4:
p in V
;
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;
( r > 0 & Ball (p,r) c= V )thus
r > 0
by A5;
Ball (p,r) c= Vreconsider 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;
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 )
; 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 )
hence
V in the topology of (TOP-REAL n)
by A1, A2, PCOMPS_1:def 4; verum