∀ {R : Type u} [inst : Ring R] {S S' : Subsemiring R} (h₁ : ∀ {x : R}, x ∈ S.carrier → -x ∈ S.carrier)
  (h₂ : ∀ {x : R}, x ∈ S'.carrier → -x ∈ S'.carrier),
  { toSubsemiring := S, neg_mem' := h₁ } ≤ { toSubsemiring := S', neg_mem' := h₂ } ↔ S ≤ S'