∀ {α : Type u_1} [inst : TopologicalSpace α] (x y : Ultrafilter α)
  (motive : (∃ x_1, ↑x ≤ nhds x_1 ∧ ↑y ≤ nhds x_1) → Prop) (a : ∃ x_1, ↑x ≤ nhds x_1 ∧ ↑y ≤ nhds x_1),
  (∀ (a : α) (hx : ↑x ≤ nhds a) (hy : ↑y ≤ nhds a), motive ⋯) → motive a