Let G and Tg be given.
Assume H: topological_group G Tg.
An exact proof term for the current goal is (T1_space_topology G Tg (topological_group_T1 G Tg H)).
∎