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.
Apply atleastp_tra with
SetAdjoin (SetAdjoin (SetAdjoin (SetAdjoin (SetAdjoin (UPair x0 x1) x2) x3) x4) x5) x6,
setsum u6 u1,
u7 leaving 2 subgoals.
Apply unknownprop_8805a75f81012de0423e9173532fc074fb73b80e451597fde52287a4721fb204 with
SetAdjoin (SetAdjoin (SetAdjoin (SetAdjoin (UPair x0 x1) x2) x3) x4) x5,
Sing x6,
u6,
u1 leaving 2 subgoals.
The subproof is completed by applying unknownprop_64283f372689c951426ae8d649fec9f376f7cbf5cb90cae78f87ad478a86b091 with x0, x1, x2, x3, x4, x5.
The subproof is completed by applying unknownprop_6f4f3b954cb736651074754cd4a7a9c9f8fdee5b2d9e8c774389a322e59d45f1 with x6.
Apply equip_atleastp with
setsum u6 u1,
ordsucc u6.
Apply equip_sym with
ordsucc u6,
setsum u6 u1.
Apply unknownprop_d631a7130d5b5dc7c63be4f6ec657039b3370cb84697eaa2bc8ab827ff606adf with
u6,
λ x7 x8 . equip x7 (setsum u6 u1).
Apply unknownprop_80fb4e499c5b9d344e7e79a37790e81cc16e6fd6cd87e88e961f3c8c4d6d418f with
u6,
u1,
u6,
u1 leaving 4 subgoals.
The subproof is completed by applying nat_6.
The subproof is completed by applying nat_1.
The subproof is completed by applying equip_ref with
u6.
The subproof is completed by applying equip_ref with
u1.