defpred S2[ object , object ] means ex D1 being set st
( D1 = X & P = D1 /\ S );
A1: for e being object st e in P holds
ex u being object st S2[e,u]
proof
let e be object ; :: thesis: ( e in P implies ex u being object st S2[e,u] )
assume e in P ; :: thesis: ex u being object st S2[e,u]
reconsider ee = e as set by TARSKI:1;
take ee /\ S ; :: thesis: S2[e,ee /\ S]
thus S2[e,ee /\ S] ; :: thesis: verum
end;
consider f being Function such that
A2: dom f = P and
A3: for e being object st e in P holds
S2[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 object ; :: 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 object 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 S2[xx,f . xx] by A3;
then x = f . xx by 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