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