theorem Th3: :: NDIFF10:3

for X, Y being RealNormSpace
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 ) )