∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : Preorder α] {x y : α}
  (motive : (∃ U, IsClopen U ∧ IsUpperSet U ∧ x ∈ U ∧ y ∉ U) → Prop)
  (x_1 : ∃ U, IsClopen U ∧ IsUpperSet U ∧ x ∈ U ∧ y ∉ U),
  (∀ (U : Set α) (hU : IsClopen U) (hU' : IsUpperSet U) (hx : x ∈ U) (hy : y ∉ U), motive ⋯) → motive x_1