defpred S₁[ set , set ] means P = X /\ S;
A1: for e being set st e in P holds
ex u being set st S₁[e,u] ;
consider f being Function such that
A2: dom f = P and
A3: for e being set st e in P holds
S₁[e,f . e] from CLASSES1:sch 1(A1);
A4: rng f is finite by A2, FINSET_1:8;
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
A5: x = xx /\ S and
A6: xx meets S ;
consider y being set such that
y in xx and
A7: y in S by A6, XBOOLE_0:3;
reconsider Xp1 = X as non empty set by A7;
A8: P is a_partition of Xp1 ;
then x = f . xx by A3, A5;
hence x in rng f by A8, A2, FUNCT_1:def 3; :: thesis: verum

end;

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