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