{α : Type u_3} →
  {motive : ConditionallyCompletePartialOrderInf α → Sort u} →
    (t : ConditionallyCompletePartialOrderInf α) →
      ([toPartialOrder : PartialOrder α] →
          [toInfSet : InfSet α] →
            (isGLB_csInf_of_directed :
                ∀ (s : Set α), DirectedOn (fun x1 x2 => x1 ≥ x2) s → s.Nonempty → BddBelow s → IsGLB s (sInf s)) →
              motive
                { toPartialOrder := toPartialOrder, toInfSet := toInfSet,
                  isGLB_csInf_of_directed := isGLB_csInf_of_directed }) →
        motive t