let G be BinContinuous TopaddGroup; :: thesis: for O being open Subset of G
for a being Element of G holds O + a is open
let O be open Subset of G; :: thesis: for a being Element of G holds O + a is open
let a be Element of G; :: thesis: O + a is open
O + a = (+ a) .: O by Th16;
hence O + a is open by TOPGRP_1:25; :: thesis: verum