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