let G be BinContinuous TopGroup; :: thesis: for F being closed Subset of G
for a being Element of G holds a * F is closed
let F be closed Subset of G; :: thesis: for a being Element of G holds a * F is closed
let a be Element of G; :: thesis: a * F is closed
a * F = (a *) .: F by Th15;
hence a * F is closed by TOPS_2:58; :: thesis: verum