let G be BinContinuous TopaddGroup; :: thesis: for A being dense Subset of G
for a being Point of G holds A + a is dense
let A be dense Subset of G; :: thesis: for a being Point of G holds A + a is dense
let a be Point of G; :: thesis: A + a is dense
(+ a) .: A = A + a by Th16;
hence A + a is dense by TOPGRP_1:28; :: thesis: verum