theorem Th36: :: GROUP_1A:354

for T being non empty TopSpace-like BinContinuous TopaddGrStr
for a, b being Element of T
for W being a_neighborhood of a + b ex A being open a_neighborhood of a ex B being open a_neighborhood of b st A + B c= W