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 )
consider r being Real such that
A1: r = 1 ;
take r ; :: thesis: ( r > 0 & Ball (v,r) c= the carrier of V )
thus r > 0 by A1; :: thesis: Ball (v,r) c= the carrier of V
thus Ball (v,r) c= the carrier of V ; :: thesis: verum