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 Th16;
hence A * a is dense by Th27; :: thesis: verum