let X, Y be RealNormSpace; :: thesis: for V being Subset of [:X,Y:] holds
( V is open iff for x being Point of X
for y being Point of Y st [x,y] in V holds
ex r1, r2 being Real st
( 0 < r1 & 0 < r2 & [:(Ball (x,r1)),(Ball (y,r2)):] c= V ) )
let V be Subset of [:X,Y:]; :: thesis: ( V is open iff for x being Point of X
for y being Point of Y st [x,y] in V holds
ex r1, r2 being Real st
( 0 < r1 & 0 < r2 & [:(Ball (x,r1)),(Ball (y,r2)):] c= V ) )

hereby :: thesis: ( ( for x being Point of X
for y being Point of Y st [x,y] in V holds
ex r1, r2 being Real st
( 0 < r1 & 0 < r2 & [:(Ball (x,r1)),(Ball (y,r2)):] c= V ) ) implies V is open )

assume A1: V is open ; :: thesis: for x being Point of X
for y being Point of Y st [x,y] in V holds
ex r1, r2 being Real st
( 0 < r1 & 0 < r2 & [:(Ball (x,r1)),(Ball (y,r2)):] c= V )
let x be Point of X; :: thesis: for y being Point of Y st [x,y] in V holds
ex r1, r2 being Real st
( 0 < r1 & 0 < r2 & [:(Ball (x,r1)),(Ball (y,r2)):] c= V )
let y be Point of Y; :: thesis: ( [x,y] in V implies ex r1, r2 being Real st
( 0 < r1 & 0 < r2 & [:(Ball (x,r1)),(Ball (y,r2)):] c= V ) )
assume [x,y] in V ; :: thesis: ex r1, r2 being Real st
( 0 < r1 & 0 < r2 & [:(Ball (x,r1)),(Ball (y,r2)):] c= V )
then consider r being Real such that
A2: ( 0 < r & [:(Ball (x,r)),(Ball (y,r)):] c= V ) by A1, NDIFF_8:23;
thus ex r1, r2 being Real st
( 0 < r1 & 0 < r2 & [:(Ball (x,r1)),(Ball (y,r2)):] c= V ) by A2; :: thesis: verum

end;

assume A3: for x being Point of X
for y being Point of Y st [x,y] in V holds
ex r1, r2 being Real st
( 0 < r1 & 0 < r2 & [:(Ball (x,r1)),(Ball (y,r2)):] c= V ) ; :: 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 A4: z in V ; :: thesis: ex s being Real st
( s > 0 & Ball (z,s) c= V )
consider x being Point of X, y being Point of Y such that
A5: z = [x,y] by PRVECT_3:18;
consider r1, r2 being Real such that
A6: ( 0 < r1 & 0 < r2 & [:(Ball (x,r1)),(Ball (y,r2)):] c= V ) by A3, A4, A5;
consider s being Real such that
A7: ( s = min (r1,r2) & s > 0 ) and
A8: Ball (z,s) c= [:(Ball (x,r1)),(Ball (y,r2)):] by A5, A6, Th2;
take s ; :: thesis: ( s > 0 & Ball (z,s) c= V )
thus ( s > 0 & Ball (z,s) c= V ) by A6, A7, A8, XBOOLE_1:1; :: thesis: verum

end;

hence V is open by NDIFF_8:20; :: thesis: verum