Proofgold Proof

pf

Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Let x3 of type ι be given.

Let x4 of type ι be given.

Let x5 of type ι be given.

Let x6 of type ι be given.

Let x7 of type ι be given.

Apply binunionI2 with SetAdjoin (SetAdjoin (SetAdjoin (SetAdjoin (SetAdjoin (UPair x0 x1) x2) x3) x4) x5) x6, Sing x7, x7.

The subproof is completed by applying SingI with x7.

■