rintro x hx
case pos.intro
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : 0 ∉ S
C : Set (Ideal R)
hC : C ⊆ Kaplansky.set S
hC₂ : IsChain (fun x x_1 => x ≤ x_1) C
h : Set.Nonempty C
I : Ideal R
hI : I ∈ C
⊢ ∀ (x : R), x ∉ ↑(sSup C) ∩ ↑S
case pos.intro
R : Type u_1
inst✝ : Semiring R
S : Subsemigroup R
hS : 0 ∉ S
C : Set (Ideal R)
hC : C ⊆ Kaplansky.set S
hC₂ : IsChain (fun x x_1 => x ≤ x_1) C
h : Set.Nonempty C
I : Ideal R
hI : I ∈ C
x : R
hx : x ∈ ↑(sSup C) ∩ ↑S
⊢ False