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