let G be UnContinuous TopaddGroup; :: thesis: for A being dense Subset of G holds - A is dense
let A be dense Subset of G; :: thesis: - A is dense
(add_inverse G) " A = - A by Th10;
hence - A is dense by TOPGRP_1:29; :: thesis: verum