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