∀ {G : Type u_2} [inst : AddGroup G] [inst_1 : TopologicalSpace G] {K : Type u_1} [inst_2 : AddGroup K]
  [inst_3 : TopologicalSpace K] {U : Set (G × K)} (U₁ : Set G) (U₂ : Set K),
  U₁ ×ˢ U₂ ⊆ U → ∀ (V : OpenAddSubgroup G), ↑V ⊆ U₁ → ∀ (W : OpenAddSubgroup K), ↑W ⊆ U₂ → ∃ W, ↑V ×ˢ ↑W ⊆ U