let X, Y be non empty TopSpace; :: thesis: for A being Subset of X

for B being Subset of Y

for V being a_neighborhood of A

for W being a_neighborhood of B holds [:V,W:] is a_neighborhood of [:A,B:]

let A be Subset of X; :: thesis: for B being Subset of Y

for V being a_neighborhood of A

for W being a_neighborhood of B holds [:V,W:] is a_neighborhood of [:A,B:]

let B be Subset of Y; :: thesis: for V being a_neighborhood of A

for W being a_neighborhood of B holds [:V,W:] is a_neighborhood of [:A,B:]

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

let W be a_neighborhood of B; :: thesis: [:V,W:] is a_neighborhood of [:A,B:]

( A c= Int V & B c= Int W ) by CONNSP_2:def 2;

then [:A,B:] c= [:(Int V),(Int W):] by ZFMISC_1:96;

hence [:A,B:] c= Int [:V,W:] by Th7; :: according to CONNSP_2:def 2 :: thesis: verum

for B being Subset of Y

for V being a_neighborhood of A

for W being a_neighborhood of B holds [:V,W:] is a_neighborhood of [:A,B:]

let A be Subset of X; :: thesis: for B being Subset of Y

for V being a_neighborhood of A

for W being a_neighborhood of B holds [:V,W:] is a_neighborhood of [:A,B:]

let B be Subset of Y; :: thesis: for V being a_neighborhood of A

for W being a_neighborhood of B holds [:V,W:] is a_neighborhood of [:A,B:]

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

let W be a_neighborhood of B; :: thesis: [:V,W:] is a_neighborhood of [:A,B:]

( A c= Int V & B c= Int W ) by CONNSP_2:def 2;

then [:A,B:] c= [:(Int V),(Int W):] by ZFMISC_1:96;

hence [:A,B:] c= Int [:V,W:] by Th7; :: according to CONNSP_2:def 2 :: thesis: verum