let G be BinContinuous TopaddGroup; :: thesis: for O being open Subset of G
for a being Element of G holds a + O is open
let O be open Subset of G; :: thesis: for a being Element of G holds a + O is open
let a be Element of G; :: thesis: a + O is open
a + O = (a +) .: O by Th15;
hence a + O is open by TOPGRP_1:25; :: thesis: verum