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:16; :: according to XBOOLE_0:def 10 :: thesis: A * O c= Int (A * O)
let x be object ; :: 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 and
A3: a in A and
A4: o in O ;
set Q = a * O;
A5: a * O c= A * O

proof

let q be object ; :: 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 ex h being Element of G st
( q = a * h & h in O ) by GROUP_2:27;
hence q in A * O by A3; :: thesis: verum

end;

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

end;

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