Theorem JoinedIn.inv

feat: add path component of the identity in a locally path connected topological group, as an open normal subgroup (#25668)