theorem Th46: :: TOPGRP_1:47

for G being BinContinuous TopGroup
for F being closed Subset of G
for a being Element of G holds a * F is closed