∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] {K : Type u_2} [inst_2 : AddGroup K]
  [inst_3 : TopologicalSpace K] (x : Set (G × K)) (motive : (∃ V W, ↑V ×ˢ ↑W ⊆ x) → Prop) (x_1 : ∃ V W, ↑V ×ˢ ↑W ⊆ x),
  (∀ (V : OpenAddSubgroup G) (W : OpenAddSubgroup K) (h : ↑V ×ˢ ↑W ⊆ x), motive ⋯) → motive x_1