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