let G be BinContinuous TopGroup; :: thesis: for O being open Subset of G
for a being Element of G holds O * a is open
let O be open Subset of G; :: thesis: for a being Element of G holds O * a is open
let a be Element of G; :: thesis: O * a is open
O * a = (* a) .: O by Th16;
hence O * a is open by Th24; :: thesis: verum