Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply atleastp_tra with
SetAdjoin (UPair x0 x1) x2,
setsum u2 u1,
u3 leaving 2 subgoals.
Apply unknownprop_8805a75f81012de0423e9173532fc074fb73b80e451597fde52287a4721fb204 with
UPair x0 x1,
Sing x2,
u2,
u1 leaving 2 subgoals.
The subproof is completed by applying unknownprop_597982e7559de2b855feaaad714998b2c76c203ae083789ba10d06918304c2af with x0, x1.
The subproof is completed by applying unknownprop_6f4f3b954cb736651074754cd4a7a9c9f8fdee5b2d9e8c774389a322e59d45f1 with x2.
Apply equip_atleastp with
setsum u2 u1,
ordsucc u2.
Apply equip_sym with
ordsucc u2,
setsum u2 u1.
Apply unknownprop_d631a7130d5b5dc7c63be4f6ec657039b3370cb84697eaa2bc8ab827ff606adf with
u2,
λ x3 x4 . equip x3 (setsum u2 u1).
Apply unknownprop_80fb4e499c5b9d344e7e79a37790e81cc16e6fd6cd87e88e961f3c8c4d6d418f with
u2,
u1,
u2,
u1 leaving 4 subgoals.
The subproof is completed by applying nat_2.
The subproof is completed by applying nat_1.
The subproof is completed by applying equip_ref with
u2.
The subproof is completed by applying equip_ref with
u1.