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

proof

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

proof

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in O * a or q in O * A )
assume q in O * a ; :: thesis: q in O * A
then ex h being Element of G st
( q = h * a & h in O ) by GROUP_2:28;
hence q in O * A by A3; :: thesis: verum

end;

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

end;

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