let X, Y be RealNormSpace; :: thesis: for V being Subset of [:X,Y:]
for D being Subset of Y st D is open & V = [: the carrier of X,D:] holds
V is open
let V be Subset of [:X,Y:]; :: thesis: for D being Subset of Y st D is open & V = [: the carrier of X,D:] holds
V is open
let D be Subset of Y; :: thesis: ( D is open & V = [: the carrier of X,D:] implies V is open )
assume A1: ( D is open & V = [: the carrier of X,D:] ) ; :: thesis: V is open
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 )

proof

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 ( x in the carrier of X & y in D ) by A1, ZFMISC_1:87;
then consider r being Real such that
A2: ( r > 0 & Ball (y,r) c= D ) by A1, NDIFF_8:20;
[:(Ball (x,r)),(Ball (y,r)):] c= V

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in [:(Ball (x,r)),(Ball (y,r)):] or z in V )
assume z in [:(Ball (x,r)),(Ball (y,r)):] ; :: thesis: z in V
then consider qx, qy being object such that
A4: ( qx in Ball (x,r) & qy in Ball (y,r) & z = [qx,qy] ) by ZFMISC_1:def 2;
thus z in V by A1, A2, A4, ZFMISC_1:87; :: thesis: verum

end;

hence ex r1, r2 being Real st
( 0 < r1 & 0 < r2 & [:(Ball (x,r1)),(Ball (y,r2)):] c= V ) by A2; :: thesis: verum

end;

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