let G be UnContinuous TopaddGroup; :: thesis: for O being open Subset of G holds - O is open
let O be open Subset of G; :: thesis: - O is open
- O = (add_inverse G) .: O by Th9;
hence - O is open by TOPGRP_1:25; :: thesis: verum