let V be RealUnitarySpace; :: thesis: for v being Point of V ex r being Real st
( r > 0 & Ball (v,r) c= the carrier of V )
let v be Point of V; :: thesis: ex r being Real st
( r > 0 & Ball (v,r) c= the carrier of V )
take r = 1; :: thesis: ( r > 0 & Ball (v,r) c= the carrier of V )
thus r > 0 ; :: thesis: Ball (v,r) c= the carrier of V
thus Ball (v,r) c= the carrier of V ; :: thesis: verum