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;
A1: the carrier of (subrelstr S) = S by YELLOW_0:def 15;
now :: thesis: for x being set st x in C | S holds
x is StableSet of (subrelstr S)
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
A2: x = c /\ S and
A3: c meets S ;
consider z being object such that
z in c and
A4: z in S by A3, XBOOLE_0:3;
A5: not subrelstr S is empty by A4, YELLOW_0:def 15;
A6: not R is empty by A4;
reconsider Rp1 = R as non empty RelStr by A4;
reconsider xp1 = x as Subset of (subrelstr S) by A1, A2, 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
A7: a in xp1 and
A8: b in xp1 and
A9: a <> b ; :: thesis: ( not a <= b & not b <= a )
A10: ( a in c & b in c ) by A7, A8, A2, XBOOLE_0:def 4;
reconsider ap1 = a, bp1 = b as Element of R by A5, A6, YELLOW_0:58;
C is Coloring of Rp1 ;
then c in C ;
then reconsider cp1 = c as Subset of R ;
A11: cp1 is stable by DILWORTH:def 12;
assume ( a <= b or b <= a ) ; :: thesis: contradiction
then ( ap1 <= bp1 or bp1 <= ap1 ) by YELLOW_0:59;
hence contradiction by A9, A10, A11; :: thesis: verum
end;
hence x is StableSet of (subrelstr S) ; :: thesis: verum
end;
hence C | S is Coloring of (subrelstr S) by A1, DILWORTH:def 12; :: thesis: verum