Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_4b1a7ff1f1af5eade46b5657f25a1ce39a3af58e2fba0b757867e511fb9aacae with
x0,
x1,
λ x2 x3 . atleastp x3 u2.
Apply setsum_1_1_2 with
λ x2 x3 . atleastp (binunion (Sing x0) (Sing x1)) x2.
Apply unknownprop_8805a75f81012de0423e9173532fc074fb73b80e451597fde52287a4721fb204 with
Sing x0,
Sing x1,
u1,
u1 leaving 2 subgoals.
The subproof is completed by applying unknownprop_6f4f3b954cb736651074754cd4a7a9c9f8fdee5b2d9e8c774389a322e59d45f1 with x0.
The subproof is completed by applying unknownprop_6f4f3b954cb736651074754cd4a7a9c9f8fdee5b2d9e8c774389a322e59d45f1 with x1.