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 )

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

hence
V is open
by Th3; :: thesis: verum
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

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

end;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

hence
ex r1, r2 being Real st
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;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

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