let R be RelStr ; :: thesis: for C being Coloring of R
for S being Subset of R holds C | S is Coloring of (subrelstr S)
let C be Coloring of R; :: thesis: for S being Subset of R holds C | S is Coloring of (subrelstr S)
let S be Subset of R; :: thesis: C | S is Coloring of (subrelstr S)
set sS = subrelstr S;
A: the carrier of (subrelstr S) = S by YELLOW_0:def 15;

now

let x be set ; :: thesis: ( x in C | S implies x is StableSet of (subrelstr S) )
assume x in C | S ; :: thesis: x is StableSet of (subrelstr S)
then consider c being Element of C such that
A1: x = c /\ S and
B1: c meets S ;
consider z being set such that
z in c and
D1: z in S by B1, XBOOLE_0:3;
E1: not subrelstr S is empty by YELLOW_0:def 15, D1;
F1: not R is empty by D1;
reconsider Rp1 = R as non empty RelStr by D1;
reconsider xp1 = x as Subset of (subrelstr S) by A, A1, XBOOLE_1:17;
xp1 is stable

proof

let a, b be Element of (subrelstr S); :: according to DILWORTH:def 2 :: thesis: ( not a in xp1 or not b in xp1 or a = b or ( not a <= b & not b <= a ) )
assume that
A2: a in xp1 and
B2: b in xp1 and
C2: a <> b ; :: thesis: ( not a <= b & not b <= a )
D2: ( a in c & b in c ) by A2, B2, A1, XBOOLE_0:def 4;
reconsider ap1 = a, bp1 = b as Element of R by E1, F1, YELLOW_0:59;
E2: C is Coloring of Rp1 ;
then c in C ;
then reconsider cp1 = c as Subset of R ;
G2: cp1 is stable by E2, DILWORTH:def 12;
assume ( a <= b or b <= a ) ; :: thesis: contradiction
then ( ap1 <= bp1 or bp1 <= ap1 ) by YELLOW_0:60;
hence contradiction by C2, D2, G2, DILWORTH:def 2; :: thesis: verum

end;

hence x is StableSet of (subrelstr S) ; :: thesis: verum

end;

hence C | S is Coloring of (subrelstr S) by A, DILWORTH:def 12; :: thesis: verum