let V be RealUnitarySpace; 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; 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; ( 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
; 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 )
verumproof
set p =
r - (dist v,u);
take
r - (dist v,u)
;
( 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:52;
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;
( w in Ball u,(r - (dist v,u)) implies w in Ball v,r )
assume
w in Ball u,
(r - (dist v,u))
;
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:22;
(dist v,u) + (dist u,w) >= dist v,
w
by BHSP_1:42;
then
dist v,
w < r
by A2, XXREAL_0:2;
hence
w in Ball v,
r
by BHSP_2:41;
verum
end;
hence
Ball u,
(r - (dist v,u)) c= Ball v,
r
by SUBSET_1:7;
verum
end;