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, XBOOLE_1:1; :: 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, XBOOLE_1:1; :: thesis: verum