set sS = subrelstr S;
consider C being Coloring of R such that
A1: C is finite by Def2;
A2: the carrier of (subrelstr S) = S by YELLOW_0:def 15;
reconsider CS = C | S as a_partition of S ;
for x being set st x in CS holds
x is StableSet of (subrelstr S)
proof
let x be set ; :: thesis: ( x in CS implies x is StableSet of (subrelstr S) )
assume x in CS ; :: thesis: x is StableSet of (subrelstr S)
then consider X being Element of C such that
A3: x = X /\ S and
A4: X meets S ;
ex y being object st
( y in X & y in S ) by A4, XBOOLE_0:3;
then X is StableSet of R by DILWORTH:def 12;
hence x is StableSet of (subrelstr S) by A3, DILWORTH:31; :: thesis: verum
end;
then CS is Coloring of (subrelstr S) by A2, DILWORTH:def 12;
hence subrelstr S is with_finite_chromatic# by A1; :: thesis: verum