Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

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

Apply unknownprop_c3fe42b21df0810041479a97b374de73f7754e07c8af1c88386a1e7dc0aad10f with setminus (binunion x0 x1) x2, binunion (setminus x0 x2) (setminus x1 x2).

Let x3 of type ι be given.

Assume H0: In x3 (setminus (binunion x0 x1) x2).

Apply unknownprop_e02b92c94ff70655b8eb0623a7ec106c0c0c9c65ac0f52f9689f2e6c9f563b5d with binunion x0 x1, x2, x3, In x3 (binunion (setminus x0 x2) (setminus x1 x2)) leaving 2 subgoals.

The subproof is completed by applying H0.

Assume H1: In x3 (binunion x0 x1).

Assume H2: nIn x3 x2.

Apply unknownprop_a497a9c4fdb392b95b688b10c74f8f445a953a0c88030ccc02fa0b24e4758231 with x0, x1, x3, In x3 (binunion (setminus x0 x2) (setminus x1 x2)) leaving 3 subgoals.

The subproof is completed by applying H1.

Assume H3: In x3 x0.

Apply unknownprop_1598d20a62a395ced156dfcc7d767ab023594ea6ef7c5e3b53cecdbebaf0ec29 with setminus x0 x2, setminus x1 x2, x3.

Apply unknownprop_3fe7f97dcb00bcf31cf989081bd8403f8f0647acc7dd719f8a7da64cd4837dac with x0, x2, x3 leaving 2 subgoals.

The subproof is completed by applying H3.

The subproof is completed by applying H2.

Assume H3: In x3 x1.

Apply unknownprop_e6919c45bef19e01f88ce072c705412578331e9a3c7532de752ffb4187ed1265 with setminus x0 x2, setminus x1 x2, x3.

Apply unknownprop_3fe7f97dcb00bcf31cf989081bd8403f8f0647acc7dd719f8a7da64cd4837dac with x1, x2, x3 leaving 2 subgoals.

The subproof is completed by applying H3.

The subproof is completed by applying H2.

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

Apply unknownprop_c3fe42b21df0810041479a97b374de73f7754e07c8af1c88386a1e7dc0aad10f with setminus x0 x2, setminus (binunion x0 x1) x2.

Let x3 of type ι be given.

Assume H0: In x3 (setminus x0 x2).

Apply unknownprop_e02b92c94ff70655b8eb0623a7ec106c0c0c9c65ac0f52f9689f2e6c9f563b5d with x0, x2, x3, In x3 (setminus (binunion x0 x1) x2) leaving 2 subgoals.

The subproof is completed by applying H0.

Assume H1: In x3 x0.

Assume H2: nIn x3 x2.

Apply unknownprop_3fe7f97dcb00bcf31cf989081bd8403f8f0647acc7dd719f8a7da64cd4837dac with binunion x0 x1, x2, x3 leaving 2 subgoals.

Apply unknownprop_1598d20a62a395ced156dfcc7d767ab023594ea6ef7c5e3b53cecdbebaf0ec29 with x0, x1, x3.

The subproof is completed by applying H1.

The subproof is completed by applying H2.

Apply unknownprop_c3fe42b21df0810041479a97b374de73f7754e07c8af1c88386a1e7dc0aad10f with setminus x1 x2, setminus (binunion x0 x1) x2.

Let x3 of type ι be given.

Assume H0: In x3 (setminus x1 x2).

Apply unknownprop_e02b92c94ff70655b8eb0623a7ec106c0c0c9c65ac0f52f9689f2e6c9f563b5d with x1, x2, x3, In x3 (setminus (binunion x0 x1) x2) leaving 2 subgoals.

The subproof is completed by applying H0.

Assume H1: In x3 x1.

Assume H2: nIn x3 x2.

Apply unknownprop_3fe7f97dcb00bcf31cf989081bd8403f8f0647acc7dd719f8a7da64cd4837dac with binunion x0 x1, x2, x3 leaving 2 subgoals.

Apply unknownprop_e6919c45bef19e01f88ce072c705412578331e9a3c7532de752ffb4187ed1265 with x0, x1, x3.

The subproof is completed by applying H1.

The subproof is completed by applying H2.

■

Proofgold Proof