let G be UnContinuous TopGroup; :: thesis: for O being open Subset of G holds O " is open
let O be open Subset of G; :: thesis: O " is open
O " = (inverse_op G) .: O by Th9;
hence O " is open by Th24; :: thesis: verum