let n be Nat; :: thesis: for V being Subset of () holds
( V in the topology of () iff for p being Point of () st p in V holds
ex r being Real st
( r > 0 & Ball (p,r) c= V ) )

let V be Subset of (); :: thesis: ( V in the topology of () iff for p being Point of () 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 (), the topology of () #) = TopSpaceMetr () by EUCLID:def 8;
A2: TopSpaceMetr () = TopStruct(# the carrier of (),() #) by PCOMPS_1:def 5;
reconsider V1 = V as Subset of () by EUCLID:67;
hereby :: thesis: ( ( for p being Point of () st p in V holds
ex r being Real st
( r > 0 & Ball (p,r) c= V ) ) implies V in the topology of () )
assume A3: V in the topology of () ; :: thesis: for p being Point of () st p in V holds
ex r being Real st
( r > 0 & Ball (p,r) c= V )

let p be Point of (); :: 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 () by EUCLID:67;
consider r being Real such that
A5: ( r > 0 & Ball (x,r) c= V1 ) by ;
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 ; :: thesis: verum
end;
assume A6: for p being Point of () st p in V holds
ex r being Real st
( r > 0 & Ball (p,r) c= V ) ; :: thesis: V in the topology of ()
for x being Element of () st x in V1 holds
ex r being Real st
( r > 0 & Ball (x,r) c= V1 )
proof
let x be Element of (); :: 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 () 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 ; :: thesis: verum
end;
hence V in the topology of () by ; :: thesis: verum