let G be BinContinuous TopGroup; :: 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 Th27; :: thesis: verum