set ss = { B where B is Subset of X : ex A being Subset of X st A ^|^ B,F } ;
defpred S₁[ set , set ] means ex a, b being set st
( X = [a,b] & F = [a,b] `2 );
A2: for x being set st x in F holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis: ( x in F implies ex y being set st S₁[x,y] )
assume x in F ; :: thesis: ex y being set st S₁[x,y]
then consider a, b being Subset of X such that
A3: x = [a,b] by Th10;
reconsider a = a, b = b as set ;
take b ; :: thesis: S₁[x,b]
take a ; :: thesis: ex b being set st
( x = [a,b] & b = [a,b] `2 )
take b ; :: thesis: ( x = [a,b] & b = [a,b] `2 )
thus ( x = [a,b] & b = [a,b] `2 ) by A3, MCART_1:def 2; :: thesis: verum

end;

consider f being Function such that
A4: dom f = F and
A5: for x being set st x in F holds
S₁[x,f . x] from CLASSES1:sch 1(A2);
A6: rng f is finite by A4, FINSET_1:26;
{ B where B is Subset of X : ex A being Subset of X st A ^|^ B,F } c= rng f

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { B where B is Subset of X : ex A being Subset of X st A ^|^ B,F } or x in rng f )
assume x in { B where B is Subset of X : ex A being Subset of X st A ^|^ B,F } ; :: thesis: x in rng f
then consider B being Subset of X such that
A7: x = B and
A8: ex A being Subset of X st A ^|^ B,F ;
consider A being Subset of X such that
A9: A ^|^ B,F by A8;
A10: [A,B] in Maximal_wrt F by A9, Def18;
then consider a, b being set such that
A11: ( [A,B] = [a,b] & f . [A,B] = [a,b] `2 ) by A5;
f . [A,B] = B by A11, MCART_1:def 2;
hence x in rng f by A4, A7, A10, FUNCT_1:12; :: thesis: verum

end;

hence saturated-subsets F is finite by A6; :: thesis: verum