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