let R be with_finite_chromatic# RelStr ; :: thesis:
let C be finite Coloring of R; :: thesis:
let c be set ; :: thesis:
assume that
AA: c in C and
A: card C = chromatic# R ; :: thesis:
assume B: 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:
set cR = the carrier of R;
AA3: union C = the carrier of R by EQREL_1:def 6;
reconsider c = c as Subset of the carrier of R by AA;
AA1: c <> {} by AA, EQREL_1:def 6;
set Cc = C \ {c};
AA2a: c in {c} by TARSKI:def 1;

suppose S1: C \ {c} is empty ; :: thesis:

consider v being set such that
A1: v in c by AA1, XBOOLE_0:def 1;
reconsider v = v as Element of R by A1;
consider d being Element of C such that
B1: d <> c and
for w being Element of R holds
( not w in Adjacent v or not w in d ) by A1, B;
0 = (card C) - (card {c}) by AA, EULER_1:5, S1, CARD_1:47;
then 0 + 1 = ((card C) - 1) + 1 by CARD_1:50;
then consider x being set such that
D1: C = {x} by CARD_2:60;
( c = x & d = x ) by AA, D1, TARSKI:def 1;
hence contradiction by B1; :: thesis:

end;

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

then reconsider Cc = C \ {c} as non empty set ;
defpred S₁[ set , set ] means 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 $2 ) ) );
P1: for e being set st e in c holds
ex u being set st S₁[e,u]

proof

let v be set ; :: thesis:
assume A1: v in c ; :: thesis:
reconsider vv = v as Element of the carrier of R by A1;
consider d being Element of C such that
B1: d <> c and
C1: for w being Element of R holds
( not w in Adjacent vv or not w in d ) by A1, B;
take d ; :: thesis:
thus S₁[v,d] by B1, C1, AA; :: thesis:

end;

consider r being Function such that
D: dom r = c and
E: for e being set st e in c holds
S₁[e,r . e] from CLASSES1:sch 1(P1);
defpred S₂[ set ] means verum;
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 set such that
Dd: d in Cc by XBOOLE_0:def 1;
Dee: d \/ (r " {d}) in { H₁(d) where d is Element of Cc : S₂[d] } by Dd;
F: { H₁(d) where d is Element of Cc : S₂[d] } c= bool the carrier of R

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { H₁(d) where d is Element of Cc : S₂[d] } ; :: thesis:
then consider d being Element of Cc such that
A1: x = d \/ (r " {d}) ;
B1: r " {d} c= c by D, RELAT_1:167;
B1a: r " {d} c= the carrier of R by B1, XBOOLE_1:1;
d in C by XBOOLE_0:def 5;
then x c= the carrier of R by A1, B1a, XBOOLE_1:8;
hence x in bool the carrier of R ; :: thesis:

end;

G: 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:

proof

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

end;

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A1a: x in the carrier of R ; :: thesis:
then consider d being set such that
A1: x in d and
B1: d in C by AA3, TARSKI:def 4;
reconsider xp1 = x as Element of the carrier of R by A1a;

per cases ;

suppose S2: d = c ; :: thesis:

then r . xp1 <> c by A1, E;
then A2: not r . xp1 in {c} by TARSKI:def 1;
r . xp1 in C by A1, S2, E;
then B2: r . xp1 in Cc by A2, XBOOLE_0:def 5;
r . xp1 in {(r . xp1)} by TARSKI:def 1;
then x in r " {(r . xp1)} by A1, S2, D, FUNCT_1:def 13;
then C2: 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 B2;
hence x in union { H₁(d) where d is Element of Cc : S₂[d] } by C2, TARSKI:def 4; :: thesis:

end;

suppose d <> c ; :: thesis:

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

end;

H: 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:
assume A in { H₁(d) where d is Element of Cc : S₂[d] } ; :: thesis:
then consider da being Element of Cc such that
B1: A = da \/ (r " {da}) ;
B1a: da in C by XBOOLE_0:def 5;
then not da is empty by EQREL_1:def 6;
hence A <> {} by B1; :: thesis:
let B be Subset of the carrier of R; :: thesis:
assume B in { H₁(d) where d is Element of Cc : S₂[d] } ; :: thesis:
then consider db being Element of Cc such that
D1: B = db \/ (r " {db}) ;
E1: db in C by XBOOLE_0:def 5;

per cases ;

suppose da = db ; :: thesis:

hence ( A = B or A misses B ) by B1, D1; :: thesis:

end;

suppose S1: da <> db ; :: thesis:

then A2a: da misses db by B1a, E1, EQREL_1:def 6;
A2b: r " {da} misses r " {db} by S1, ZFMISC_1:17, FUNCT_1:141;
assume A <> B ; :: thesis:
assume A meets B ; :: thesis:
then consider x being set such that
B2: x in A and
C2: x in B by XBOOLE_0:3;

per cases by B2, C2, B1, D1, XBOOLE_0:def 3;

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

hence contradiction by A2a, XBOOLE_0:3; :: thesis:

end;

suppose that S2a: x in da and
S2b: x in r " {db} ; :: thesis:

A3: da <> c by AA2a, XBOOLE_0:def 5;
r " {db} c= c by D, RELAT_1:167;
then da meets c by S2a, S2b, XBOOLE_0:3;
hence contradiction by A3, B1a, AA, EQREL_1:def 6; :: thesis:

end;

suppose that S2a: x in r " {da} and
S2b: x in db ; :: thesis:

A3: db <> c by AA2a, XBOOLE_0:def 5;
r " {da} c= c by D, RELAT_1:167;
then db meets c by S2a, S2b, XBOOLE_0:3;
hence contradiction by A3, E1, AA, EQREL_1:def 6; :: thesis:

end;

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

hence contradiction by A2b, XBOOLE_0:3; :: thesis:

end;

reconsider D = { H₁(d) where d is Element of Cc : S₂[d] } as a_partition of the carrier of R by F, G, H, EQREL_1:def 6;

now

let x be set ; :: thesis:
assume A1: x in D ; :: thesis:
then reconsider S = x as Subset of R ;
consider d being Element of Cc such that
B1: x = d \/ (r " {d}) by A1;
C1: r " {d} c= c by D, RELAT_1:167;
D1: d in C by XBOOLE_0:def 5;
E1: d is StableSet of R by D1, DILWORTH:def 12;
F1: c is StableSet of R by AA, DILWORTH:def 12;
S is stable

proof

let a, b be Element of R; :: according to DILWORTH:def 2 :: thesis:
assume that
A2: a in S and
B2: b in S and
C2: a <> b ; :: thesis:

per cases by A2, B2, B1, XBOOLE_0:def 3;

suppose ( a in d & b in d ) ; :: thesis:

hence ( not a <= b & not b <= a ) by E1, C2, DILWORTH:def 2; :: thesis:

end;

suppose that A3: a in d and
B3: b in r " {d} ; :: thesis:

r . b in {d} by B3, FUNCT_1:def 13;
then r . b = d by TARSKI:def 1;
then not a in Adjacent b by A3, C1, B3, E;
then ( not a < b & not b < a ) by LAdjset;
hence ( not a <= b & not b <= a ) by C2, ORDERS_2:def 10; :: thesis:

end;

suppose that A3: a in r " {d} and
B3: b in d ; :: thesis:

r . a in {d} by A3, FUNCT_1:def 13;
then r . a = d by TARSKI:def 1;
then not b in Adjacent a by B3, C1, A3, E;
then ( not a < b & not b < a ) by LAdjset;
hence ( not a <= b & not b <= a ) by C2, ORDERS_2:def 10; :: thesis:

end;

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

hence ( not a <= b & not b <= a ) by C1, F1, C2, DILWORTH:def 2; :: thesis:

end;

hence x is StableSet of R ; :: thesis:

end;

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

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in rng s ; :: thesis:
then consider d being set such that
A1: d in dom s and
B1: y = s . d by FUNCT_1:def 5;
y = d \/ (r " {d}) by sA, sB, A1, B1;
hence y in D by A1, sA; :: thesis:

end;

then reconsider s = s as Function of Cc,D by sA, FUNCT_2:4;
s1: s is one-to-one

proof

let x1, x2 be set ; :: according to FUNCT_1:def 8 :: thesis:
assume that
A1: x1 in dom s and
B1: x2 in dom s and
C1: s . x1 = s . x2 ; :: thesis:
D1: s . x1 = x1 \/ (r " {x1}) by A1, sB;
E1: s . x2 = x2 \/ (r " {x2}) by B1, sB;
thus x1 c= x2 :: according to XBOOLE_0:def 10 :: thesis:

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A2: x in x1 ; :: thesis:
then B2: x in s . x1 by D1, XBOOLE_0:def 3;

per cases by B2, C1, E1, XBOOLE_0:def 3;

suppose x in x2 ; :: thesis:

hence x in x2 ; :: thesis:

end;

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

A3a: r " {x2} c= dom r by RELAT_1:167;
B3: x1 in C by A1, XBOOLE_0:def 5;
then reconsider x1 = x1 as Subset of the carrier of R ;
x1 meets c by A3a, S3, D, A2, XBOOLE_0:3;
then x1 = c by B3, AA, EQREL_1:def 6;
hence x in x2 by AA2a, A1, XBOOLE_0:def 5; :: thesis:

end;

thus x2 c= x1 :: thesis:

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A2: x in x2 ; :: thesis:
then B2: x in s . x2 by E1, XBOOLE_0:def 3;

per cases by B2, C1, D1, XBOOLE_0:def 3;

suppose x in x1 ; :: thesis:

hence x in x1 ; :: thesis:

end;

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

A3a: r " {x1} c= dom r by RELAT_1:167;
B3: x2 in C by B1, XBOOLE_0:def 5;
then reconsider x2 = x2 as Subset of the carrier of R ;
x2 meets c by A3a, S3, D, A2, XBOOLE_0:3;
then x2 = c by B3, AA, EQREL_1:def 6;
hence x in x1 by AA2a, XBOOLE_0:def 5, B1; :: thesis:

end;

D c= rng s

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in D ; :: thesis:
then consider d being Element of Cc such that
A1: x = d \/ (r " {d}) ;
s . d = d \/ (r " {d}) by sB;
hence x in rng s by A1, sA, FUNCT_1:def 5; :: thesis:

end;

then D = rng s by sr, XBOOLE_0:def 10;
then s is onto by FUNCT_2:def 3;
then J: card Cc = card D by s1, Dee, EULER_1:12;
then D is finite ;
hence contradiction by I, J, A, Lchro; :: thesis:

end;