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:] 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; :: thesis: 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; :: thesis: 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:]; :: thesis: ( 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 ) ; :: thesis: 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 ; :: thesis: ( 0 < r2 & [:(Ball (x,r2)),(Ball (y,r2)):] c= V )
thus 0 < r2 by A3; :: thesis: [:(Ball (x,r2)),(Ball (y,r2)):] c= V
thus [:(Ball (x,r2)),(Ball (y,r2)):] c= V by A2, A3, XBOOLE_1:1; :: thesis: verum