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 Th15;
hence a + A is dense by TOPGRP_1:28; :: thesis: verum