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 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 A1: ( v in Ball u,r & v in Ball w,p ) by XBOOLE_0:def 4;
then consider s being Real such that
A2: ( s > 0 & Ball v,s c= Ball u,r ) by Th35;
consider t being Real such that
A3: ( t > 0 & Ball v,t c= Ball w,p ) by A1, Th35;
take q = min s,t; :: thesis: ( Ball v,q c= Ball u,r & Ball v,q c= Ball w,p )
( q <= s & q > 0 ) by A2, A3, XXREAL_0:15, XXREAL_0:17;
then Ball v,q c= Ball v,s by Th33;
hence Ball v,q c= Ball u,r by A2, XBOOLE_1:1; :: thesis: Ball v,q c= Ball w,p
( q <= t & q > 0 ) by A2, A3, XXREAL_0:15, XXREAL_0:17;
then Ball v,q c= Ball v,t by Th33;
hence Ball v,q c= Ball w,p by A3, XBOOLE_1:1; :: thesis: verum