let G be BinContinuous TopGroup; :: thesis: for A, O being Subset of G st O is open holds
A * O is open
let A, O be Subset of G; :: thesis: ( O is open implies A * O is open )
assume A1: O is open ; :: thesis: A * O is open
Int (A * O) = A * O

proof

thus Int (A * O) c= A * O by TOPS_1:44; :: according to XBOOLE_0:def 10 :: thesis: A * O c= Int (A * O)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A * O or x in Int (A * O) )
assume x in A * O ; :: thesis: x in Int (A * O)
then consider a, o being Element of G such that
A2: ( x = a * o & a in A & o in O ) ;
set Q = a * O;
A4: a * O c= A * O

proof

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in a * O or q in A * O )
assume q in a * O ; :: thesis: q in A * O
then consider h being Element of G such that
A5: ( q = a * h & h in O ) by GROUP_2:33;
thus q in A * O by A2, A5; :: thesis: verum

end;

x in a * O by A2, GROUP_2:33;
hence x in Int (A * O) by A1, A4, TOPS_1:54; :: thesis: verum

end;

hence A * O is open ; :: thesis: verum