let V be RealUnitarySpace; :: thesis: for u, v, w being Point of V
for r, p being Real st v in (Ball (u,r)) /\ (Ball (w,p)) holds
ex q being Real st
( Ball (v,q) c= Ball (u,r) & Ball (v,q) c= Ball (w,p) )
let u, v, w be Point of V; :: thesis: for r, p being Real st v in (Ball (u,r)) /\ (Ball (w,p)) holds
ex q being Real st
( Ball (v,q) c= Ball (u,r) & Ball (v,q) c= Ball (w,p) )
let r, p be Real; :: thesis: ( v in (Ball (u,r)) /\ (Ball (w,p)) implies ex q being Real st
( Ball (v,q) c= Ball (u,r) & Ball (v,q) c= Ball (w,p) ) )
assume A1: v in (Ball (u,r)) /\ (Ball (w,p)) ; :: thesis: ex q being Real st
( Ball (v,q) c= Ball (u,r) & Ball (v,q) c= Ball (w,p) )
then v in Ball (u,r) by XBOOLE_0:def 4;
then consider s being Real such that
s > 0 and
A2: Ball (v,s) c= Ball (u,r) by Th35;
v in Ball (w,p) by A1, XBOOLE_0:def 4;
then consider t being Real such that
t > 0 and
A3: Ball (v,t) c= Ball (w,p) by Th35;
take q = min (s,t); :: thesis: ( Ball (v,q) c= Ball (u,r) & Ball (v,q) c= Ball (w,p) )
Ball (v,q) c= Ball (v,s) by Th33, XXREAL_0:17;
hence Ball (v,q) c= Ball (u,r) by A2; :: thesis: Ball (v,q) c= Ball (w,p)
Ball (v,q) c= Ball (v,t) by Th33, XXREAL_0:17;
hence Ball (v,q) c= Ball (w,p) by A3; :: thesis: verum