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