{α : Type u_2} →
  [inst : TopologicalSpace α] →
    [inst_1 : LE α] →
      {motive : ClopenUpperSet α → Sort u} →
        (t : ClopenUpperSet α) →
          ((toClopens : TopologicalSpace.Clopens α) →
              (upper' : IsUpperSet toClopens.carrier) → motive { toClopens := toClopens, upper' := upper' }) →
            motive t