let G be BinContinuous TopaddGroup; :: 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