Let x be given.

Assume Hx.

Let alpha be given.

Assume Ha.

Apply SNoEq_I to the current goal.

Let beta be given.

Assume Hb: beta ∈ alpha.

We will prove beta ∈ x ∩ SNoElts_ alpha ↔ beta ∈ x.

Apply iffI to the current goal.

Assume H1: beta ∈ x ∩ SNoElts_ alpha.

An exact proof term for the current goal is binintersectE1 x (SNoElts_ alpha) beta H1.

Assume H1: beta ∈ x.

Apply binintersectI to the current goal.

An exact proof term for the current goal is H1.

We will prove beta ∈ alpha ∪ {SetAdjoin beta {1}|beta ∈ alpha}.

Apply binunionI1 to the current goal.

An exact proof term for the current goal is Hb.

∎