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