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

end;

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

end;

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