let n be Nat; :: thesis: for p being Point of ()
for S being open Subset of () st p in S holds
ex B being ball Subset of () st
( B c= S & p in B )

let p be Point of (); :: thesis: for S being open Subset of () st p in S holds
ex B being ball Subset of () st
( B c= S & p in B )

let S be open Subset of (); :: thesis: ( p in S implies ex B being ball Subset of () st
( B c= S & p in B ) )

assume A1: p in S ; :: thesis: ex B being ball Subset of () st
( B c= S & p in B )

A2: TopStruct(# the carrier of (), the topology of () #) = TopSpaceMetr () by EUCLID:def 8;
A3: S in Family_open_set () by ;
reconsider x = p as Element of () by A2;
consider r being Real such that
A4: ( r > 0 & Ball (x,r) c= S ) by ;
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 () 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 ; :: thesis: verum