let C be closed Subset of (TOP-REAL 2); :: thesis: for p being Point of (Euclid 2) st p in BDD C holds
ex r being Real st
( r > 0 & Ball (p,r) c= BDD C )
let p be Point of (Euclid 2); :: thesis: ( p in BDD C implies ex r being Real st
( r > 0 & Ball (p,r) c= BDD C ) )
set W = Int (BDD C);
assume p in BDD C ; :: thesis: ex r being Real st
( r > 0 & Ball (p,r) c= BDD C )
then p in Int (BDD C) by TOPS_1:23;
then consider r being Real such that
A1: r > 0 and
A2: Ball (p,r) c= BDD C by GOBOARD6:5;
reconsider r = r as Real ;
take r ; :: thesis: ( r > 0 & Ball (p,r) c= BDD C )
thus ( r > 0 & Ball (p,r) c= BDD C ) by A1, A2; :: thesis: verum