let I be set ; :: thesis: for M being V8() ManySortedSet of I
for B being V32() ManySortedSubset of M ex C being V8() V32() ManySortedSubset of M st B c= C
let M be V8() ManySortedSet of I; :: thesis: for B being V32() ManySortedSubset of M ex C being V8() V32() ManySortedSubset of M st B c= C
let B be V32() ManySortedSubset of M; :: thesis: ex C being V8() V32() ManySortedSubset of M st B c= C
defpred S₁[ set , set ] means ex a being Element of M . $1 st $2 = {a} \/ (B . $1);

A1: now

let i be set ; :: thesis: ( i in I implies ex j being set st S₁[i,j] )
assume i in I ; :: thesis: ex j being set st S₁[i,j]
consider a being Element of M . i;
take j = {a} \/ (B . i); :: thesis: S₁[i,j]
thus S₁[i,j] ; :: thesis: verum

end;

consider C being ManySortedSet of I such that
A2: for i being set st i in I holds
S₁[i,C . i] from PBOOLE:sch 3(A1);
A3: C is ManySortedSubset of M

proof

let i be set ; :: according to PBOOLE:def 5,PBOOLE:def 23 :: thesis: ( not i in I or C . i c= M . i )
assume A4: i in I ; :: thesis: C . i c= M . i
then consider a being Element of M . i such that
A5: C . i = {a} \/ (B . i) by A2;
let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in C . i or q in M . i )
assume q in C . i ; :: thesis: q in M . i
then A6: ( q in {a} or q in B . i ) by A5, XBOOLE_0:def 3;
B c= M by PBOOLE:def 23;
then B . i c= M . i by A4, PBOOLE:def 5;
then A7: ( q = a or q in M . i ) by A6, TARSKI:def 1;
not M . i is empty by A4;
hence q in M . i by A7; :: thesis: verum

end;

A8: C is finite-yielding

proof

let i be set ; :: according to FINSET_1:def 4 :: thesis: ( not i in I or C . i is finite )
assume A9: i in I ; :: thesis: C . i is finite
then reconsider b = B . i as finite set by FINSET_1:def 4;
consider a being Element of M . i such that
A10: C . i = {a} \/ (B . i) by A2, A9;
{a} \/ b is finite ;
hence C . i is finite by A10; :: thesis: verum

end;

C is non-empty

proof

let i be set ; :: according to PBOOLE:def 16 :: thesis: ( not i in I or not C . i is empty )
assume i in I ; :: thesis: not C . i is empty
then ex a being Element of M . i st C . i = {a} \/ (B . i) by A2;
hence not C . i is empty ; :: thesis: verum

end;

then reconsider C = C as V8() V32() ManySortedSubset of M by A3, A8;
take C ; :: thesis: B c= C
let i be set ; :: according to PBOOLE:def 5 :: thesis: ( not i in I or B . i c= C . i )
assume i in I ; :: thesis: B . i c= C . i
then ex a being Element of M . i st C . i = {a} \/ (B . i) by A2;
hence B . i c= C . i by XBOOLE_1:7; :: thesis: verum