let G be UnContinuous TopGroup; :: thesis: for A being dense Subset of G holds A " is dense
let A be dense Subset of G; :: thesis: A " is dense
(inverse_op G) " A = A " by Th11;
hence A " is dense by Th29; :: thesis: verum