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

A1: now :: thesis: for i being object st i in I holds
ex j being object st S₁[i,j]

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

end;

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

proof

let i be object ; :: according to PBOOLE:def 2,PBOOLE:def 18 :: 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 object ; :: 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 18;
then B . i c= M . i by A4;
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 object ; :: according to FINSET_1:def 5 :: thesis: ( not i in I or C . i is finite )
assume A9: i in I ; :: thesis: C . i is finite
reconsider b = B . i as finite set ;
consider a being Element of M . i such that
A10: C . i = {a} \/ (B . i) by A2, A9;
thus C . i is finite by A10; :: thesis: verum

end;

C is non-empty

proof

let i be object ; :: according to PBOOLE:def 13 :: 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 non-empty finite-yielding ManySortedSubset of M by A3, A8;
take C ; :: thesis: B c= C
let i be object ; :: according to PBOOLE:def 2 :: 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