let X, Y be non empty TopSpace; :: thesis: for x being Point of
for y being Point of
for V being Subset of holds
( V is a_neighborhood of [:{x},{y}:] iff V is a_neighborhood of [x,y] )
let x be Point of ; :: thesis: for y being Point of
for V being Subset of holds
( V is a_neighborhood of [:{x},{y}:] iff V is a_neighborhood of [x,y] )
let y be Point of ; :: thesis: for V being Subset of holds
( V is a_neighborhood of [:{x},{y}:] iff V is a_neighborhood of [x,y] )
let V be Subset of ; :: 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:35;
hence V is a_neighborhood of [x,y] by CONNSP_2:10; :: 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:10;
hence V is a_neighborhood of [:{x},{y}:] by ZFMISC_1:35; :: thesis: verum