theorem Th48: :: TOPGRP_1:49

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