let V be RealUnitarySpace; :: thesis: for v, u being Point of V
for r being Real st u in Ball (v,r) holds
ex p being Real st
( p > 0 & Ball (u,p) c= Ball (v,r) )
let v, u be Point of V; :: thesis: for r being Real st u in Ball (v,r) holds
ex p being Real st
( p > 0 & Ball (u,p) c= Ball (v,r) )
let r be Real; :: thesis: ( u in Ball (v,r) implies ex p being Real st
( p > 0 & Ball (u,p) c= Ball (v,r) ) )
assume u in Ball (v,r) ; :: thesis: ex p being Real st
( p > 0 & Ball (u,p) c= Ball (v,r) )
then A1: dist (v,u) < r by BHSP_2:41;
thus ex p being Real st
( p > 0 & Ball (u,p) c= Ball (v,r) ) :: thesis: verum

proof

set p = r - (dist (v,u));
take r - (dist (v,u)) ; :: thesis: ( r - (dist (v,u)) > 0 & Ball (u,(r - (dist (v,u)))) c= Ball (v,r) )
thus r - (dist (v,u)) > 0 by A1, XREAL_1:50; :: thesis: Ball (u,(r - (dist (v,u)))) c= Ball (v,r)
for w being Point of V st w in Ball (u,(r - (dist (v,u)))) holds
w in Ball (v,r)

proof

let w be Point of V; :: thesis: ( w in Ball (u,(r - (dist (v,u)))) implies w in Ball (v,r) )
assume w in Ball (u,(r - (dist (v,u)))) ; :: thesis: w in Ball (v,r)
then dist (u,w) < r - (dist (v,u)) by BHSP_2:41;
then A2: (dist (v,u)) + (dist (u,w)) < r by XREAL_1:20;
(dist (v,u)) + (dist (u,w)) >= dist (v,w) by BHSP_1:35;
then dist (v,w) < r by A2, XXREAL_0:2;
hence w in Ball (v,r) by BHSP_2:41; :: thesis: verum

end;

hence Ball (u,(r - (dist (v,u)))) c= Ball (v,r) ; :: thesis: verum

end;