{α : Type u_1} →
  [inst : TopologicalSpace α] →
    [inst_1 : Preorder α] →
      {motive : HasUpperLowerClosure α → Sort u} →
        ((isUpperSet_closure : ∀ (s : Set α), IsUpperSet s → IsUpperSet (closure s)) →
            (isLowerSet_closure : ∀ (s : Set α), IsLowerSet s → IsLowerSet (closure s)) →
              (isOpen_upperClosure : ∀ (s : Set α), IsOpen s → IsOpen ↑(upperClosure s)) →
                (isOpen_lowerClosure : ∀ (s : Set α), IsOpen s → IsOpen ↑(lowerClosure s)) → motive ⋯) →
          (t : HasUpperLowerClosure α) → motive t