let n be Nat; :: thesis: for p being Point of (TOP-REAL n)

for S being open Subset of (TOP-REAL n) st p in S holds

ex B being ball Subset of (TOP-REAL n) st

( B c= S & p in B )

let p be Point of (TOP-REAL n); :: thesis: for S being open Subset of (TOP-REAL n) st p in S holds

ex B being ball Subset of (TOP-REAL n) st

( B c= S & p in B )

let S be open Subset of (TOP-REAL n); :: thesis: ( p in S implies ex B being ball Subset of (TOP-REAL n) st

( B c= S & p in B ) )

assume A1: p in S ; :: thesis: ex B being ball Subset of (TOP-REAL n) st

( B c= S & p in B )

A2: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;

A3: S in Family_open_set (Euclid n) by A2, PRE_TOPC:def 2;

reconsider x = p as Element of (Euclid n) by A2;

consider r being Real such that

A4: ( r > 0 & Ball (x,r) c= S ) by A1, A3, PCOMPS_1:def 4;

reconsider r = r as positive Real by A4;

reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

reconsider B = Ball (p,r) as ball Subset of (TOP-REAL n) by Def1;

take B ; :: thesis: ( B c= S & p in B )

reconsider p1 = p as Point of (TOP-REAL n1) ;

Ball (x,r) = Ball (p1,r) by TOPREAL9:13;

hence ( B c= S & p in B ) by A4, GOBOARD6:1; :: thesis: verum

for S being open Subset of (TOP-REAL n) st p in S holds

ex B being ball Subset of (TOP-REAL n) st

( B c= S & p in B )

let p be Point of (TOP-REAL n); :: thesis: for S being open Subset of (TOP-REAL n) st p in S holds

ex B being ball Subset of (TOP-REAL n) st

( B c= S & p in B )

let S be open Subset of (TOP-REAL n); :: thesis: ( p in S implies ex B being ball Subset of (TOP-REAL n) st

( B c= S & p in B ) )

assume A1: p in S ; :: thesis: ex B being ball Subset of (TOP-REAL n) st

( B c= S & p in B )

A2: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;

A3: S in Family_open_set (Euclid n) by A2, PRE_TOPC:def 2;

reconsider x = p as Element of (Euclid n) by A2;

consider r being Real such that

A4: ( r > 0 & Ball (x,r) c= S ) by A1, A3, PCOMPS_1:def 4;

reconsider r = r as positive Real by A4;

reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

reconsider B = Ball (p,r) as ball Subset of (TOP-REAL n) by Def1;

take B ; :: thesis: ( B c= S & p in B )

reconsider p1 = p as Point of (TOP-REAL n1) ;

Ball (x,r) = Ball (p1,r) by TOPREAL9:13;

hence ( B c= S & p in B ) by A4, GOBOARD6:1; :: thesis: verum