theorem Th52: :: TOPGRP_1:53

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