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