Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Apply set_ext with binunion x0 (binunion x1 x2), binunion (binunion x0 x1) x2 leaving 2 subgoals.

Let x3 of type ι be given.

Assume H0: x3 ∈ binunion x0 (binunion x1 x2).

Apply binunionE with x0, binunion x1 x2, x3, x3 ∈ binunion (binunion x0 x1) x2 leaving 3 subgoals.

The subproof is completed by applying H0.

Assume H1: x3 ∈ x0.

Apply binunionI1 with binunion x0 x1, x2, x3.

Apply binunionI1 with x0, x1, x3.

The subproof is completed by applying H1.

Assume H1: x3 ∈ binunion x1 x2.

Apply binunionE with x1, x2, x3, x3 ∈ binunion (binunion x0 x1) x2 leaving 3 subgoals.

The subproof is completed by applying H1.

Assume H2: x3 ∈ x1.

Apply binunionI1 with binunion x0 x1, x2, x3.

Apply binunionI2 with x0, x1, x3.

The subproof is completed by applying H2.

Assume H2: x3 ∈ x2.

Apply binunionI2 with binunion x0 x1, x2, x3.

The subproof is completed by applying H2.

Let x3 of type ι be given.

Assume H0: x3 ∈ binunion (binunion x0 x1) x2.

Apply binunionE with binunion x0 x1, x2, x3, x3 ∈ binunion x0 (binunion x1 x2) leaving 3 subgoals.

The subproof is completed by applying H0.

Assume H1: x3 ∈ binunion x0 x1.

Apply binunionE with x0, x1, x3, x3 ∈ binunion x0 (binunion x1 x2) leaving 3 subgoals.

The subproof is completed by applying H1.

Assume H2: x3 ∈ x0.

Apply binunionI1 with x0, binunion x1 x2, x3.

The subproof is completed by applying H2.

Assume H2: x3 ∈ x1.

Apply binunionI2 with x0, binunion x1 x2, x3.

Apply binunionI1 with x1, x2, x3.

The subproof is completed by applying H2.

Assume H1: x3 ∈ x2.

Apply binunionI2 with x0, binunion x1 x2, x3.

Apply binunionI2 with x1, x2, x3.

The subproof is completed by applying H1.

■

Proofgold Proof