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 ) )
assume A1: p in BDD C ; :: thesis: ex r being Real st
( r > 0 & Ball p,r c= BDD C )
set W = Int (BDD C);
p in Int (BDD C) by A1, TOPS_1:55;
then consider r being real number such that
A2: ( r > 0 & Ball p,r c= BDD C ) by GOBOARD6:8;
reconsider r = r as Real by XREAL_0:def 1;
take r ; :: thesis: ( r > 0 & Ball p,r c= BDD C )
thus ( r > 0 & Ball p,r c= BDD C ) by A2; :: thesis: verum