defpred S₁[ set , set ] means ex a, b being set 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 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
A2: 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 A2, MCART_1:def 2; :: thesis: verum

end;

consider f being Function such that
A3: dom f = F and
A4: for x being set 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 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
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, Def18;
then ex a, b being set st
( [A,B] = [a,b] & f . [A,B] = [a,b] `2 ) by A4;
then f . [A,B] = B by MCART_1:def 2;
hence x in rng f by A3, A6, A9, FUNCT_1:12; :: thesis: verum

end;

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