let G be BinContinuous TopGroup; :: thesis: for A being dense Subset of
for a being Point of holds A * a is dense
let A be dense Subset of ; :: thesis: for a being Point of holds A * a is dense
let a be Point of ; :: thesis: A * a is dense
(* a) .: A = A * a by Th17;
hence A * a is dense by Th28; :: thesis: verum