for G being BinContinuous TopGroup
for A, O being Subset of G st O is open holds
O * A is open