let X, Y be non empty TopSpace; :: thesis: for x being Point of X

for y being Point of Y

for V being a_neighborhood of x

for W being a_neighborhood of y holds [:V,W:] is a_neighborhood of [x,y]

let x be Point of X; :: thesis: for y being Point of Y

for V being a_neighborhood of x

for W being a_neighborhood of y holds [:V,W:] is a_neighborhood of [x,y]

let y be Point of Y; :: thesis: for V being a_neighborhood of x

for W being a_neighborhood of y holds [:V,W:] is a_neighborhood of [x,y]

let V be a_neighborhood of x; :: thesis: for W being a_neighborhood of y holds [:V,W:] is a_neighborhood of [x,y]

let W be a_neighborhood of y; :: thesis: [:V,W:] is a_neighborhood of [x,y]

( x in Int V & y in Int W ) by CONNSP_2:def 1;

then [x,y] in [:(Int V),(Int W):] by ZFMISC_1:87;

hence [x,y] in Int [:V,W:] by Th7; :: according to CONNSP_2:def 1 :: thesis: verum

for y being Point of Y

for V being a_neighborhood of x

for W being a_neighborhood of y holds [:V,W:] is a_neighborhood of [x,y]

let x be Point of X; :: thesis: for y being Point of Y

for V being a_neighborhood of x

for W being a_neighborhood of y holds [:V,W:] is a_neighborhood of [x,y]

let y be Point of Y; :: thesis: for V being a_neighborhood of x

for W being a_neighborhood of y holds [:V,W:] is a_neighborhood of [x,y]

let V be a_neighborhood of x; :: thesis: for W being a_neighborhood of y holds [:V,W:] is a_neighborhood of [x,y]

let W be a_neighborhood of y; :: thesis: [:V,W:] is a_neighborhood of [x,y]

( x in Int V & y in Int W ) by CONNSP_2:def 1;

then [x,y] in [:(Int V),(Int W):] by ZFMISC_1:87;

hence [x,y] in Int [:V,W:] by Th7; :: according to CONNSP_2:def 1 :: thesis: verum