theorem Th51: :: TOPGRP_1:52

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