let X, Y be RealNormSpace; :: thesis: for x being Point of X
for y being Point of Y
for z being Point of [:X,Y:]
for r1, r2 being Real st 0 < r1 & 0 < r2 & z = [x,y] holds
ex s being Real st
( s = min (r1,r2) & s > 0 & Ball (z,s) c= [:(Ball (x,r1)),(Ball (y,r2)):] )
let x be Point of X; :: thesis: for y being Point of Y
for z being Point of [:X,Y:]
for r1, r2 being Real st 0 < r1 & 0 < r2 & z = [x,y] holds
ex s being Real st
( s = min (r1,r2) & s > 0 & Ball (z,s) c= [:(Ball (x,r1)),(Ball (y,r2)):] )
let y be Point of Y; :: thesis: for z being Point of [:X,Y:]
for r1, r2 being Real st 0 < r1 & 0 < r2 & z = [x,y] holds
ex s being Real st
( s = min (r1,r2) & s > 0 & Ball (z,s) c= [:(Ball (x,r1)),(Ball (y,r2)):] )
let z be Point of [:X,Y:]; :: thesis: for r1, r2 being Real st 0 < r1 & 0 < r2 & z = [x,y] holds
ex s being Real st
( s = min (r1,r2) & s > 0 & Ball (z,s) c= [:(Ball (x,r1)),(Ball (y,r2)):] )
let r1, r2 be Real; :: thesis: ( 0 < r1 & 0 < r2 & z = [x,y] implies ex s being Real st
( s = min (r1,r2) & s > 0 & Ball (z,s) c= [:(Ball (x,r1)),(Ball (y,r2)):] ) )
assume A1: ( 0 < r1 & 0 < r2 & z = [x,y] ) ; :: thesis: ex s being Real st
( s = min (r1,r2) & s > 0 & Ball (z,s) c= [:(Ball (x,r1)),(Ball (y,r2)):] )
take s = min (r1,r2); :: thesis: ( s = min (r1,r2) & s > 0 & Ball (z,s) c= [:(Ball (x,r1)),(Ball (y,r2)):] )
Ball (z,s) c= [:(Ball (x,r1)),(Ball (y,r2)):]

proof

let z1 be object ; :: according to TARSKI:def 3 :: thesis: ( not z1 in Ball (z,s) or z1 in [:(Ball (x,r1)),(Ball (y,r2)):] )
assume A3: z1 in Ball (z,s) ; :: thesis: z1 in [:(Ball (x,r1)),(Ball (y,r2)):]
then reconsider z1 = z1 as Point of [:X,Y:] ;
A4: ex z2 being Point of [:X,Y:] st
( z2 = z1 & ||.(z - z2).|| < s ) by A3;
consider x1 being Point of X, y1 being Point of Y such that
A5: z1 = [x1,y1] by PRVECT_3:18;
- z1 = [(- x1),(- y1)] by A5, PRVECT_3:18;
then z - z1 = [(x - x1),(y - y1)] by A1, PRVECT_3:18;
then ( ||.(x - x1).|| <= ||.(z - z1).|| & ||.(y - y1).|| <= ||.(z - z1).|| ) by NDIFF_8:21;
then A6: ( ||.(x - x1).|| < s & ||.(y - y1).|| < s ) by A4, XXREAL_0:2;
( s <= r1 & s <= r2 ) by XXREAL_0:17;
then ( ||.(x - x1).|| < r1 & ||.(y - y1).|| < r2 ) by A6, XXREAL_0:2;
then ( x1 in Ball (x,r1) & y1 in Ball (y,r2) ) ;
hence z1 in [:(Ball (x,r1)),(Ball (y,r2)):] by A5, ZFMISC_1:87; :: thesis: verum

end;

hence ( s = min (r1,r2) & s > 0 & Ball (z,s) c= [:(Ball (x,r1)),(Ball (y,r2)):] ) by A1, XXREAL_0:15; :: thesis: verum