{R : Type u_1} →
  [inst : Bornology R] →
    [inst_1 : Add R] →
      {motive : BoundedAdd R → Sort u} →
        ((isBounded_add :
              ∀ {s t : Set R}, Bornology.IsBounded s → Bornology.IsBounded t → Bornology.IsBounded (s + t)) →
            motive ⋯) →
          (t : BoundedAdd R) → motive t