∀ (G : Type u_1) [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G] (x : G)
  (motive : x ∈ AddSubgroup.pathComponentZero G → Prop) (x_1 : x ∈ AddSubgroup.pathComponentZero G),
  (∀ (γ : Path 0 x), motive ⋯) → motive x_1