∀ {S : Type u_1} {R : outParam (Type u)} [inst : NonAssocSemiring R] [inst_1 : SetLike S R],
  (∀ {s : S} {a b : R}, a ∈ s → b ∈ s → a * b ∈ s) →
    (∀ (s : S), 1 ∈ s) → (∀ {s : S} {a b : R}, a ∈ s → b ∈ s → a + b ∈ s) → (∀ (s : S), 0 ∈ s) → SubsemiringClass S R