let X, Y be non empty TopSpace; :: thesis: for x being Point of X
for y being Point of Y
for V being Subset of [:X,Y:] holds
( V is a_neighborhood of [:{x},{y}:] iff V is a_neighborhood of [x,y] )
let x be Point of X; :: thesis: for y being Point of Y
for V being Subset of [:X,Y:] holds
( V is a_neighborhood of [:{x},{y}:] iff V is a_neighborhood of [x,y] )
let y be Point of Y; :: thesis: for V being Subset of [:X,Y:] holds
( V is a_neighborhood of [:{x},{y}:] iff V is a_neighborhood of [x,y] )
let V be Subset of [:X,Y:]; :: thesis: ( V is a_neighborhood of [:{x},{y}:] iff V is a_neighborhood of [x,y] )
hereby :: thesis: ( V is a_neighborhood of [x,y] implies V is a_neighborhood of [:{x},{y}:] )
assume V is a_neighborhood of [:{x},{y}:] ; :: thesis: V is a_neighborhood of [x,y]
then V is a_neighborhood of {[x,y]} by ZFMISC_1:29;
hence V is a_neighborhood of [x,y] by CONNSP_2:8; :: thesis: verum
end;
assume V is a_neighborhood of [x,y] ; :: thesis: V is a_neighborhood of [:{x},{y}:]
then V is a_neighborhood of {[x,y]} by CONNSP_2:8;
hence V is a_neighborhood of [:{x},{y}:] by ZFMISC_1:29; :: thesis: verum