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