Let x be given.

Assume Hx.

Let α be given.

Assume Ha.

Apply SNoEq_I to the current goal.

Let β be given.

Assume Hb: β ∈ α.

We will prove β ∈ x ∩ SNoElts_ α ↔ β ∈ x.

Apply iffI to the current goal.

Assume H1: β ∈ x ∩ SNoElts_ α.

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

Assume H1: β ∈ x.

Apply binintersectI to the current goal.

An exact proof term for the current goal is H1.

We will prove β ∈ α ∪ {SetAdjoin β {1}|β ∈ α}.

Apply binunionI1 to the current goal.

An exact proof term for the current goal is Hb.

∎