let G be UnContinuous TopaddGroup; :: thesis: for F being closed Subset of G holds - F is closed
let F be closed Subset of G; :: thesis: - F is closed
- F = (add_inverse G) .: F by Th9;
hence - F is closed by TOPS_2:58; :: thesis: verum