Comeagre subgroup completeness argument
= Comeagre subgroup completeness argument
A dense additive subgroup of a complete metrizable topological group cannot be proper if it is <comeagre>. Every translate is comeagre and meets the subgroup, so every translating element is a difference of two subgroup elements. Applied to a <topologically complete> normed space inside its completion, this proves that its original norm is complete.