{R : Type u} →
  [inst : NonUnitalNonAssocRing R] →
    (carrier : Set R) →
      (∀ {a b : R}, a ∈ carrier → b ∈ carrier → a + b ∈ carrier) →
        0 ∈ carrier →
          (∀ {a b : R}, a ∈ carrier → b ∈ carrier → a * b ∈ carrier) →
            (∀ {x : R}, x ∈ carrier → -x ∈ carrier) → NonUnitalSubring R