let X, Y be non empty TopSpace; 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; 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; 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:]; ( V is a_neighborhood of [:{x},{y}:] iff V is a_neighborhood of [x,y] )
assume
V is a_neighborhood of [x,y]
; 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; verum