theorem ThW37: :: GROUP_1A:355

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