theorem Th51: :: GROUP_1A:369

for G being BinContinuous TopaddGroup
for A, O being Subset of G st O is open holds
O + A is open