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