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