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