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