let G be BinContinuous TopGroup; :: 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 Th24; :: thesis: verum