let X, Y be RealNormSpace; for x being Point of X
for y being Point of Y
for V being Subset of [:X,Y:] st V is open & [x,y] in V holds
ex r being Real st
( 0 < r & [:(Ball (x,r)),(Ball (y,r)):] c= V )
let x be Point of X; for y being Point of Y
for V being Subset of [:X,Y:] st V is open & [x,y] in V holds
ex r being Real st
( 0 < r & [:(Ball (x,r)),(Ball (y,r)):] c= V )
let y be Point of Y; for V being Subset of [:X,Y:] st V is open & [x,y] in V holds
ex r being Real st
( 0 < r & [:(Ball (x,r)),(Ball (y,r)):] c= V )
let V be Subset of [:X,Y:]; ( V is open & [x,y] in V implies ex r being Real st
( 0 < r & [:(Ball (x,r)),(Ball (y,r)):] c= V ) )
assume A1:
( V is open & [x,y] in V )
; ex r being Real st
( 0 < r & [:(Ball (x,r)),(Ball (y,r)):] c= V )
reconsider z = [x,y] as Point of [:X,Y:] ;
consider r being Real such that
A2:
( r > 0 & Ball (z,r) c= V )
by A1, NORMSP27;
consider r2 being Real such that
A3:
( 0 < r2 & r2 < r & [:(Ball (x,r2)),(Ball (y,r2)):] c= Ball (z,r) )
by A2, NORMSP31;
take
r2
; ( 0 < r2 & [:(Ball (x,r2)),(Ball (y,r2)):] c= V )
thus
0 < r2
by A3; [:(Ball (x,r2)),(Ball (y,r2)):] c= V
thus
[:(Ball (x,r2)),(Ball (y,r2)):] c= V
by A2, A3, XBOOLE_1:1; verum