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)):]

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

hence
( s = min (r1,r2) & s > 0 & Ball (z,s) c= [:(Ball (x,r1)),(Ball (y,r2)):] )
by A1, XXREAL_0:15; :: thesis: verum
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;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