for G being UnContinuous TopGroup
for O being open Subset of G holds O " is open