defpred S₁[ set , set ] means P = X /\ S;
P: for e being set st e in P holds
ex u being set st S₁[e,u] ;
consider f being Function such that
A: dom f = P and
B: for e being set st e in P holds
S₁[e,f . e] from CLASSES1:sch 1(P);
C: rng f is finite by A, FINSET_1:26;
P | S c= rng f

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in P | S or x in rng f )
assume x in P | S ; :: thesis: x in rng f
then consider xx being Element of P such that
A1: x = xx /\ S and
B1: xx meets S ;
consider y being set such that
y in xx and
D1: y in S by B1, XBOOLE_0:3;
reconsider Xp1 = X as non empty set by D1;
E1: P is a_partition of Xp1 ;
then x = f . xx by B, A1;
hence x in rng f by E1, A, FUNCT_1:def 5; :: thesis: verum

end;

hence P | S is finite by C; :: thesis: verum