Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Apply set_ext with
binunion x0 x1,
binunion x0 (setminus x1 x0) leaving 2 subgoals.
Let x4 of type ι be given.
Apply xm with
x4 ∈ x0,
x4 ∈ binunion x0 (setminus x1 x0) leaving 2 subgoals.
Assume H3: x4 ∈ x0.
Apply binunionI1 with
x0,
setminus x1 x0,
x4.
The subproof is completed by applying H3.
Apply binunionE with
x0,
x1,
x4,
x4 ∈ binunion x0 (setminus x1 x0) leaving 3 subgoals.
The subproof is completed by applying H2.
Assume H4: x4 ∈ x0.
Apply FalseE with
x4 ∈ binunion x0 (setminus x1 x0).
Apply H3.
The subproof is completed by applying H4.
Assume H4: x4 ∈ x1.
Apply binunionI2 with
x0,
setminus x1 x0,
x4.
Apply setminusI with
x1,
x0,
x4 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H3.
Let x4 of type ι be given.
Apply binunionE with
x0,
setminus x1 x0,
x4,
x4 ∈ binunion x0 x1 leaving 3 subgoals.
The subproof is completed by applying H2.
Assume H3: x4 ∈ x0.
Apply binunionI1 with
x0,
x1,
x4.
The subproof is completed by applying H3.
Apply binunionI2 with
x0,
x1,
x4.
Apply setminusE1 with
x1,
x0,
x4.
The subproof is completed by applying H3.
Apply L2 with
λ x4 x5 . atleastp x5 (setsum x2 x3).
Apply unknownprop_94b237fc7b7d3bf1a0a078f7d057802d281bf3c46c36fd56a85d339ac0f07170 with
x0,
setminus x1 x0,
x2,
x3 leaving 3 subgoals.
The subproof is completed by applying H0.
Apply atleastp_tra with
setminus x1 x0,
x1,
x3 leaving 2 subgoals.
Apply Subq_atleastp with
setminus x1 x0,
x1.
The subproof is completed by applying setminus_Subq with x1, x0.
The subproof is completed by applying H1.
Let x4 of type ι be given.
Assume H3: x4 ∈ x0.
Apply setminusE2 with
x1,
x0,
x4 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H3.