theorem Th45: :: TOPGRP_1:46

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