Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Assume H2:
∀ x4 . x4 ∈ x2 ⟶ nIn x4 x3.
Apply unknownprop_8c033b5532b5ecb975cda388e43db69e003e5159ad10f70a2cd946604e0cb0f6 with
x0,
x2,
atleastp (setsum x0 x1) (binunion x2 x3) leaving 2 subgoals.
The subproof is completed by applying H0.
Let x4 of type ι be given.
Assume H3: x4 ⊆ x2.
Apply unknownprop_8c033b5532b5ecb975cda388e43db69e003e5159ad10f70a2cd946604e0cb0f6 with
x1,
x3,
atleastp (setsum x0 x1) (binunion x2 x3) leaving 2 subgoals.
The subproof is completed by applying H1.
Let x5 of type ι be given.
Assume H5: x5 ⊆ x3.
Apply atleastp_tra with
setsum x0 x1,
binunion x4 x5,
binunion x2 x3 leaving 2 subgoals.
Apply equip_atleastp with
setsum x0 x1,
binunion x4 x5.
Apply equip_sym with
binunion x4 x5,
setsum x0 x1.
Apply unknownprop_8fed54475e70b18fbe9db03f1a81cd38ab9b210f0bea8d2bb706323c288b83da with
x4,
x5,
x0,
x1 leaving 3 subgoals.
Apply equip_sym with
x0,
x4.
The subproof is completed by applying H4.
Apply equip_sym with
x1,
x5.
The subproof is completed by applying H6.
Let x6 of type ι be given.
Assume H7: x6 ∈ x4.
Assume H8: x6 ∈ x5.
Apply H2 with
x6 leaving 2 subgoals.
Apply H3 with
x6.
The subproof is completed by applying H7.
Apply H5 with
x6.
The subproof is completed by applying H8.
Apply Subq_atleastp with
binunion x4 x5,
binunion x2 x3.
Apply binunion_Subq_min with
x4,
x5,
binunion x2 x3 leaving 2 subgoals.
Apply Subq_tra with
x4,
x2,
binunion x2 x3 leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying binunion_Subq_1 with x2, x3.
Apply Subq_tra with
x5,
x3,
binunion x2 x3 leaving 2 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying binunion_Subq_2 with x2, x3.