let G be BinContinuous TopaddGroup; :: 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 Th27;
hence q in A + O by A3; :: thesis: verum

end;

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

end;

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