let R be with_finite_chromatic# RelStr ; :: thesis: for C being finite Coloring of R
for c being set st c in C & card C = chromatic# R holds
ex v being Element of R st
( v in c & ( for d being Element of C st d <> c holds
ex w being Element of R st
( w in Adjacent v & w in d ) ) )
let C be finite Coloring of R; :: thesis: for c being set st c in C & card C = chromatic# R holds
ex v being Element of R st
( v in c & ( for d being Element of C st d <> c holds
ex w being Element of R st
( w in Adjacent v & w in d ) ) )
let c be set ; :: thesis: ( c in C & card C = chromatic# R implies ex v being Element of R st
( v in c & ( for d being Element of C st d <> c holds
ex w being Element of R st
( w in Adjacent v & w in d ) ) ) )
assume that
A1: c in C and
A2: card C = chromatic# R ; :: thesis: ex v being Element of R st
( v in c & ( for d being Element of C st d <> c holds
ex w being Element of R st
( w in Adjacent v & w in d ) ) )
assume A3: for v being Element of R holds
( not v in c or ex d being Element of C st
( d <> c & ( for w being Element of R holds
( not w in Adjacent v or not w in d ) ) ) ) ; :: thesis: contradiction
set cR = the carrier of R;
A4: union C = the carrier of R by EQREL_1:def 4;
reconsider c = c as Subset of the carrier of R by A1;
A5: c <> {} by A1;
set Cc = C \ {c};
A6: c in {c} by TARSKI:def 1;

per cases ( C \ {c} is empty or not C \ {c} is empty ) ;

suppose A7: C \ {c} is empty ; :: thesis: contradiction

consider v being object such that
A8: v in c by A5, XBOOLE_0:def 1;
reconsider v = v as Element of R by A8;
consider d being Element of C such that
A9: d <> c and
for w being Element of R holds
( not w in Adjacent v or not w in d ) by A8, A3;
0 = (card C) - (card {c}) by A1, A7, CARD_1:27, EULER_1:4;
then 0 + 1 = ((card C) - 1) + 1 by CARD_1:30;
then consider x being object such that
A10: C = {x} by CARD_2:42;
( c = x & d = x ) by A1, A10, TARSKI:def 1;
hence contradiction by A9; :: thesis: verum

end;

suppose not C \ {c} is empty ; :: thesis: contradiction

then reconsider Cc = C \ {c} as non empty set ;
defpred S₂[ object , object ] means ex D2 being set st
( D2 = $2 & ( for vv being Element of the carrier of R st $1 = vv holds
( $2 <> c & $2 in C & ( for w being Element of R holds
( not w in Adjacent vv or not w in D2 ) ) ) ) );
A11: for e being object st e in c holds
ex u being object st S₂[e,u]

proof

let v be object ; :: thesis: ( v in c implies ex u being object st S₂[v,u] )
assume A12: v in c ; :: thesis: ex u being object st S₂[v,u]
reconsider vv = v as Element of the carrier of R by A12;
consider d being Element of C such that
A13: d <> c and
A14: for w being Element of R holds
( not w in Adjacent vv or not w in d ) by A12, A3;
take d ; :: thesis: S₂[v,d]
take d ; :: thesis: ( d = d & ( for vv being Element of the carrier of R st v = vv holds
( d <> c & d in C & ( for w being Element of R holds
( not w in Adjacent vv or not w in d ) ) ) ) )
thus ( d = d & ( for vv being Element of the carrier of R st v = vv holds
( d <> c & d in C & ( for w being Element of R holds
( not w in Adjacent vv or not w in d ) ) ) ) ) by A13, A14, A1; :: thesis: verum

end;

consider r being Function such that
A15: dom r = c and
A16: for e being object st e in c holds
S₂[e,r . e] from CLASSES1:sch 1(A11);
deffunc H₁( set ) -> set = $1 \/ (r " {$1});
reconsider Cc = Cc as non empty finite set ;
set D = { H₁(d) where d is Element of Cc : S₁[d] } ;
consider d being object such that
A17: d in Cc by XBOOLE_0:def 1;
reconsider d = d as set by TARSKI:1;
A18: d \/ (r " {d}) in { H₁(d) where d is Element of Cc : S₁[d] } by A17;
A19: { H₁(d) where d is Element of Cc : S₁[d] } c= bool the carrier of R

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { H₁(d) where d is Element of Cc : S₁[d] } or x in bool the carrier of R )
reconsider xx = x as set by TARSKI:1;
assume x in { H₁(d) where d is Element of Cc : S₁[d] } ; :: thesis: x in bool the carrier of R
then consider d being Element of Cc such that
A20: x = d \/ (r " {d}) ;
A21: r " {d} c= c by A15, RELAT_1:132;
A22: r " {d} c= the carrier of R by A21, XBOOLE_1:1;
d in C by XBOOLE_0:def 5;
then xx c= the carrier of R by A20, A22, XBOOLE_1:8;
hence x in bool the carrier of R ; :: thesis: verum

end;

A23: union { H₁(d) where d is Element of Cc : S₁[d] } = the carrier of R

proof

thus union { H₁(d) where d is Element of Cc : S₁[d] } c= the carrier of R :: according to XBOOLE_0:def 10 :: thesis: the carrier of R c= union { H₁(d) where d is Element of Cc : S₁[d] }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union { H₁(d) where d is Element of Cc : S₁[d] } or x in the carrier of R )
assume x in union { H₁(d) where d is Element of Cc : S₁[d] } ; :: thesis: x in the carrier of R
then consider Y being set such that
A24: x in Y and
A25: Y in { H₁(d) where d is Element of Cc : S₁[d] } by TARSKI:def 4;
thus x in the carrier of R by A24, A25, A19; :: thesis: verum

end;

thus the carrier of R c= union { H₁(d) where d is Element of Cc : S₁[d] } :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of R or x in union { H₁(d) where d is Element of Cc : S₁[d] } )
assume A26: x in the carrier of R ; :: thesis: x in union { H₁(d) where d is Element of Cc : S₁[d] }
then consider d being set such that
A27: x in d and
A28: d in C by A4, TARSKI:def 4;
reconsider xp1 = x as Element of the carrier of R by A26;

per cases ( d = c or d <> c ) ;

suppose A29: d = c ; :: thesis: x in union { H₁(d) where d is Element of Cc : S₁[d] }

then A30: S₂[xp1,r . xp1] by A27, A16;
then r . xp1 <> c ;
then A31: not r . xp1 in {c} by TARSKI:def 1;
r . xp1 in C by A30;
then A32: r . xp1 in Cc by A31, XBOOLE_0:def 5;
r . xp1 in {(r . xp1)} by TARSKI:def 1;
then x in r " {(r . xp1)} by A27, A29, A15, FUNCT_1:def 7;
then A33: x in (r . xp1) \/ (r " {(r . xp1)}) by XBOOLE_0:def 3;
(r . xp1) \/ (r " {(r . xp1)}) in { H₁(d) where d is Element of Cc : S₁[d] } by A32;
hence x in union { H₁(d) where d is Element of Cc : S₁[d] } by A33, TARSKI:def 4; :: thesis: verum

end;

suppose d <> c ; :: thesis: x in union { H₁(d) where d is Element of Cc : S₁[d] }

then not d in {c} by TARSKI:def 1;
then d in Cc by A28, XBOOLE_0:def 5;
then A34: d \/ (r " {d}) in { H₁(d) where d is Element of Cc : S₁[d] } ;
x in d \/ (r " {d}) by A27, XBOOLE_0:def 3;
hence x in union { H₁(d) where d is Element of Cc : S₁[d] } by A34, TARSKI:def 4; :: thesis: verum

end;

end;

end;

end;

A35: for A being Subset of the carrier of R st A in { H₁(d) where d is Element of Cc : S₁[d] } holds
( A <> {} & ( for B being Subset of the carrier of R holds
( not B in { H₁(d) where d is Element of Cc : S₁[d] } or A = B or A misses B ) ) )

proof

let A be Subset of the carrier of R; :: thesis: ( A in { H₁(d) where d is Element of Cc : S₁[d] } implies ( A <> {} & ( for B being Subset of the carrier of R holds
( not B in { H₁(d) where d is Element of Cc : S₁[d] } or A = B or A misses B ) ) ) )
assume A in { H₁(d) where d is Element of Cc : S₁[d] } ; :: thesis: ( A <> {} & ( for B being Subset of the carrier of R holds
( not B in { H₁(d) where d is Element of Cc : S₁[d] } or A = B or A misses B ) ) )
then consider da being Element of Cc such that
A36: A = da \/ (r " {da}) ;
A37: da in C by XBOOLE_0:def 5;
then not da is empty ;
hence A <> {} by A36; :: thesis: for B being Subset of the carrier of R holds
( not B in { H₁(d) where d is Element of Cc : S₁[d] } or A = B or A misses B )
let B be Subset of the carrier of R; :: thesis: ( not B in { H₁(d) where d is Element of Cc : S₁[d] } or A = B or A misses B )
assume B in { H₁(d) where d is Element of Cc : S₁[d] } ; :: thesis: ( A = B or A misses B )
then consider db being Element of Cc such that
A38: B = db \/ (r " {db}) ;
A39: db in C by XBOOLE_0:def 5;

per cases ( da = db or da <> db ) ;

suppose da = db ; :: thesis: ( A = B or A misses B )

hence ( A = B or A misses B ) by A36, A38; :: thesis: verum

end;

suppose A40: da <> db ; :: thesis: ( A = B or A misses B )

then A41: da misses db by A37, A39, EQREL_1:def 4;
A42: r " {da} misses r " {db} by A40, FUNCT_1:71, ZFMISC_1:11;
assume A <> B ; :: thesis: A misses B
assume A meets B ; :: thesis: contradiction
then consider x being object such that
A43: x in A and
A44: x in B by XBOOLE_0:3;

per cases ( ( x in da & x in db ) or ( x in da & x in r " {db} ) or ( x in r " {da} & x in db ) or ( x in r " {da} & x in r " {db} ) ) by A43, A44, A36, A38, XBOOLE_0:def 3;

suppose ( x in da & x in db ) ; :: thesis: contradiction

hence contradiction by A41, XBOOLE_0:3; :: thesis: verum

end;

suppose that A45: x in da and
A46: x in r " {db} ; :: thesis: contradiction

A47: da <> c by A6, XBOOLE_0:def 5;
r " {db} c= c by A15, RELAT_1:132;
then da meets c by A45, A46, XBOOLE_0:3;
hence contradiction by A47, A37, A1, EQREL_1:def 4; :: thesis: verum

end;

suppose that A48: x in r " {da} and
A49: x in db ; :: thesis: contradiction

A50: db <> c by A6, XBOOLE_0:def 5;
r " {da} c= c by A15, RELAT_1:132;
then db meets c by A48, A49, XBOOLE_0:3;
hence contradiction by A50, A39, A1, EQREL_1:def 4; :: thesis: verum

end;

suppose ( x in r " {da} & x in r " {db} ) ; :: thesis: contradiction

hence contradiction by A42, XBOOLE_0:3; :: thesis: verum

end;

end;

end;

end;

end;

reconsider D = { H₁(d) where d is Element of Cc : S₁[d] } as a_partition of the carrier of R by A19, A23, A35, EQREL_1:def 4;

now :: thesis: for x being set st x in D holds
x is StableSet of R

let x be set ; :: thesis: ( x in D implies x is StableSet of R )
assume A51: x in D ; :: thesis: x is StableSet of R
then reconsider S = x as Subset of R ;
consider d being Element of Cc such that
A52: x = d \/ (r " {d}) by A51;
A53: r " {d} c= c by A15, RELAT_1:132;
A54: d in C by XBOOLE_0:def 5;
A55: d is StableSet of R by A54, DILWORTH:def 12;
A56: c is StableSet of R by A1, DILWORTH:def 12;
S is stable

proof

let a, b be Element of R; :: according to DILWORTH:def 2 :: thesis: ( not a in S or not b in S or a = b or ( not a <= b & not b <= a ) )
assume that
A57: a in S and
A58: b in S and
A59: a <> b ; :: thesis: ( not a <= b & not b <= a )

per cases ( ( a in d & b in d ) or ( a in d & b in r " {d} ) or ( a in r " {d} & b in d ) or ( a in r " {d} & b in r " {d} ) ) by A57, A58, A52, XBOOLE_0:def 3;

suppose ( a in d & b in d ) ; :: thesis: ( not a <= b & not b <= a )

hence ( not a <= b & not b <= a ) by A55, A59, DILWORTH:def 2; :: thesis: verum

end;

suppose that A60: a in d and
A61: b in r " {d} ; :: thesis: ( not a <= b & not b <= a )

r . b in {d} by A61, FUNCT_1:def 7;
then A62: r . b = d by TARSKI:def 1;
S₂[b,r . b] by A53, A61, A16;
then not a in Adjacent b by A60, A62;
then ( not a < b & not b < a ) by Def6;
hence ( not a <= b & not b <= a ) by A59, ORDERS_2:def 6; :: thesis: verum

end;

suppose that A63: a in r " {d} and
A64: b in d ; :: thesis: ( not a <= b & not b <= a )

r . a in {d} by A63, FUNCT_1:def 7;
then A65: r . a = d by TARSKI:def 1;
S₂[a,r . a] by A53, A63, A16;
then not b in Adjacent a by A64, A65;
then ( not a < b & not b < a ) by Def6;
hence ( not a <= b & not b <= a ) by A59, ORDERS_2:def 6; :: thesis: verum

end;

suppose ( a in r " {d} & b in r " {d} ) ; :: thesis: ( not a <= b & not b <= a )

hence ( not a <= b & not b <= a ) by A53, A56, A59, DILWORTH:def 2; :: thesis: verum

end;

end;

end;

hence x is StableSet of R ; :: thesis: verum

end;

then reconsider D = D as Coloring of R by DILWORTH:def 12;
card Cc = (card C) - (card {c}) by A1, EULER_1:4;
then (card Cc) + 1 = ((card C) - 1) + 1 by CARD_1:30;
then A66: card Cc < card C by NAT_1:13;
deffunc H₂( set ) -> set = $1 \/ (r " {$1});
consider s being Function such that
A67: dom s = Cc and
A68: for x being set st x in Cc holds
s . x = H₂(x) from FUNCT_1:sch 5();
A69: rng s c= D

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng s or y in D )
assume y in rng s ; :: thesis: y in D
then consider d being object such that
A70: d in dom s and
A71: y = s . d by FUNCT_1:def 3;
reconsider d = d as set by TARSKI:1;
y = d \/ (r " {d}) by A67, A68, A70, A71;
hence y in D by A70, A67; :: thesis: verum

end;

then reconsider s = s as Function of Cc,D by A67, FUNCT_2:2;
A72: s is one-to-one

proof

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom s or not x2 in dom s or not s . x1 = s . x2 or x1 = x2 )
assume that
A73: x1 in dom s and
A74: x2 in dom s and
A75: s . x1 = s . x2 ; :: thesis: x1 = x2
reconsider x1 = x1, x2 = x2 as set by TARSKI:1;
A76: s . x1 = x1 \/ (r " {x1}) by A73, A68;
A77: s . x2 = x2 \/ (r " {x2}) by A74, A68;
A78: x1 c= x2

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in x1 or x in x2 )
assume A79: x in x1 ; :: thesis: x in x2
then A80: x in s . x1 by A76, XBOOLE_0:def 3;

per cases ( x in x2 or x in r " {x2} ) by A80, A75, A77, XBOOLE_0:def 3;

suppose x in x2 ; :: thesis: x in x2

hence x in x2 ; :: thesis: verum

end;

suppose A81: x in r " {x2} ; :: thesis: x in x2

A82: r " {x2} c= dom r by RELAT_1:132;
A83: x1 in C by A73, XBOOLE_0:def 5;
then reconsider x1 = x1 as Subset of the carrier of R ;
x1 meets c by A82, A81, A15, A79, XBOOLE_0:3;
then x1 = c by A83, A1, EQREL_1:def 4;
hence x in x2 by A6, A73, XBOOLE_0:def 5; :: thesis: verum

end;

end;

end;

x2 c= x1

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in x2 or x in x1 )
assume A84: x in x2 ; :: thesis: x in x1
then A85: x in s . x2 by A77, XBOOLE_0:def 3;

per cases ( x in x1 or x in r " {x1} ) by A85, A75, A76, XBOOLE_0:def 3;

suppose x in x1 ; :: thesis: x in x1

hence x in x1 ; :: thesis: verum

end;

suppose A86: x in r " {x1} ; :: thesis: x in x1

A87: r " {x1} c= dom r by RELAT_1:132;
A88: x2 in C by A74, XBOOLE_0:def 5;
then reconsider x2 = x2 as Subset of the carrier of R ;
x2 meets c by A87, A86, A15, A84, XBOOLE_0:3;
then x2 = c by A88, A1, EQREL_1:def 4;
hence x in x1 by A6, A74, XBOOLE_0:def 5; :: thesis: verum

end;

end;

end;

hence x1 = x2 by A78, XBOOLE_0:def 10; :: thesis: verum

end;

D c= rng s

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in D or x in rng s )
assume x in D ; :: thesis: x in rng s
then consider d being Element of Cc such that
A89: x = d \/ (r " {d}) ;
s . d = d \/ (r " {d}) by A68;
hence x in rng s by A89, A67, FUNCT_1:def 3; :: thesis: verum

end;

then D = rng s by A69;
then s is onto by FUNCT_2:def 3;
then A90: card Cc = card D by A72, A18, EULER_1:11;
then D is finite ;
hence contradiction by A66, A90, A2, Def3; :: thesis: verum

end;

end;