let X, Y be RealNormSpace; :: thesis: for x being Point of X
for y being Point of Y
for V being Subset of [:X,Y:]
for r being Real st V = [:(Ball (x,r)),(Ball (y,r)):] holds
V is open
let x be Point of X; :: thesis: for y being Point of Y
for V being Subset of [:X,Y:]
for r being Real st V = [:(Ball (x,r)),(Ball (y,r)):] holds
V is open
let y be Point of Y; :: thesis: for V being Subset of [:X,Y:]
for r being Real st V = [:(Ball (x,r)),(Ball (y,r)):] holds
V is open
let V be Subset of [:X,Y:]; :: thesis: for r being Real st V = [:(Ball (x,r)),(Ball (y,r)):] holds
V is open
let r be Real; :: thesis: ( V = [:(Ball (x,r)),(Ball (y,r)):] implies V is open )
assume A1: V = [:(Ball (x,r)),(Ball (y,r)):] ; :: thesis: V is open
for z being Point of [:X,Y:] st z in V holds
ex s being Real st
( s > 0 & Ball (z,s) c= V )

proof

let z be Point of [:X,Y:]; :: thesis: ( z in V implies ex s being Real st
( s > 0 & Ball (z,s) c= V ) )
assume A2: z in V ; :: thesis: ex s being Real st
( s > 0 & Ball (z,s) c= V )
consider x1 being Point of X, y1 being Point of Y such that
A3: z = [x1,y1] by PRVECT_3:18;
A4: ( x1 in Ball (x,r) & y1 in Ball (y,r) ) by A1, A2, A3, ZFMISC_1:87;
A5: ex p being Point of X st
( x1 = p & ||.(x - p).|| < r ) by A4;
A6: ex p being Point of Y st
( y1 = p & ||.(y - p).|| < r ) by A4;
set r1 = r - ||.(x - x1).||;
set r2 = r - ||.(y - y1).||;
A7: 0 < r - ||.(x - x1).|| by A5, XREAL_1:50;
A8: 0 < r - ||.(y - y1).|| by A6, XREAL_1:50;
reconsider s = min ((r - ||.(x - x1).||),(r - ||.(y - y1).||)) as Real ;
A9: 0 < s by A7, A8, XXREAL_0:15;
A10: s <= r - ||.(x - x1).|| by XXREAL_0:17;
A11: s <= r - ||.(y - y1).|| by XXREAL_0:17;
Ball (z,s) c= V

proof

let w be object ; :: according to TARSKI:def 3 :: thesis: ( not w in Ball (z,s) or w in V )
assume A12: w in Ball (z,s) ; :: thesis: w in V
then reconsider q = w as Point of [:X,Y:] ;
A13: ex t being Point of [:X,Y:] st
( q = t & ||.(z - t).|| < s ) by A12;
consider qx being Point of X, qy being Point of Y such that
A14: q = [qx,qy] by PRVECT_3:18;
- q = [(- qx),(- qy)] by A14, PRVECT_3:18;
then z - q = [(x1 - qx),(y1 - qy)] by A3, PRVECT_3:18;
then ( ||.(x1 - qx).|| <= ||.(z - q).|| & ||.(y1 - qy).|| <= ||.(z - q).|| ) by NORMSP35;
then A16: ( ||.(x1 - qx).|| < s & ||.(y1 - qy).|| < s ) by A13, XXREAL_0:2;
(x - x1) + (x1 - qx) = ((x - x1) + x1) - qx by RLVECT_1:28
.= x - qx by RLVECT_4:1 ;
then A17: ||.(x - qx).|| <= ||.(x - x1).|| + ||.(x1 - qx).|| by NORMSP_1:def 1;
A18: ||.(x - x1).|| + ||.(x1 - qx).|| < ||.(x - x1).|| + s by A16, XREAL_1:8;
||.(x - x1).|| + s <= ||.(x - x1).|| + (r - ||.(x - x1).||) by A10, XREAL_1:7;
then ||.(x - x1).|| + ||.(x1 - qx).|| < r by A18, XXREAL_0:2;
then ||.(x - qx).|| < r by A17, XXREAL_0:2;
then A19: qx in Ball (x,r) ;
(y - y1) + (y1 - qy) = ((y - y1) + y1) - qy by RLVECT_1:28
.= y - qy by RLVECT_4:1 ;
then A20: ||.(y - qy).|| <= ||.(y - y1).|| + ||.(y1 - qy).|| by NORMSP_1:def 1;
A21: ||.(y - y1).|| + ||.(y1 - qy).|| < ||.(y - y1).|| + s by A16, XREAL_1:8;
||.(y - y1).|| + s <= ||.(y - y1).|| + (r - ||.(y - y1).||) by A11, XREAL_1:7;
then ||.(y - y1).|| + ||.(y1 - qy).|| < r by A21, XXREAL_0:2;
then ||.(y - qy).|| < r by A20, XXREAL_0:2;
then qy in Ball (y,r) ;
hence w in V by A1, A14, A19, ZFMISC_1:87; :: thesis: verum

end;

hence ex s being Real st
( s > 0 & Ball (z,s) c= V ) by A9; :: thesis: verum

end;

hence V is open by NORMSP27; :: thesis: verum