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 Th10;
hence A " is dense by Th28; :: thesis: verum