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

proof

let x be object ; :: thesis: ( x in F implies ex y being object st S₁[x,y] )
assume x in F ; :: thesis: ex y being object st S₁[x,y]
then consider a, b being Subset of X such that
A2: x = [a,b] by Th9;
reconsider a = a, b = b as set ;
take b ; :: thesis: S₁[x,b]
take a ; :: thesis: ex b being object 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 A2; :: thesis: verum

end;

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

proof

let x be object ; :: 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
A6: x = B and
A7: ex A being Subset of X st A ^|^ B,F ;
consider A being Subset of X such that
A8: A ^|^ B,F by A7;
A9: [A,B] in Maximal_wrt F by A8;
then A10: ex a, b being object st
( [A,B] = [a,b] & f . [A,B] = [a,b] `2 ) by A4;
f . [A,B] = B by A10;
hence x in rng f by A3, A6, A9, FUNCT_1:3; :: thesis: verum

end;

rng f is finite by A3, FINSET_1:8;
hence saturated-subsets F is finite by A5; :: thesis: verum