{α : Type u_8} →
  {motive : CompleteSemilatticeSup α → Sort u} →
    (t : CompleteSemilatticeSup α) →
      ([toPartialOrder : PartialOrder α] →
          [toSupSet : SupSet α] →
            (isLUB_sSup : ∀ (s : Set α), IsLUB s (sSup s)) →
              motive { toPartialOrder := toPartialOrder, toSupSet := toSupSet, isLUB_sSup := isLUB_sSup }) →
        motive t