let X, Y be non empty TopSpace; 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; 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; 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; for W being a_neighborhood of B holds [:V,W:] is a_neighborhood of [:A,B:]
let W be a_neighborhood of B; [: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; CONNSP_2:def 2 verum