theorem Th49: :: TOPGRP_1:50

for G being BinContinuous TopGroup
for O being open Subset of G
for a being Element of G holds a * O is open