let G be finitely_colorable SimpleGraph; :: thesis:
let C be finite Coloring of G; :: thesis:
let c be set ; :: thesis:
assume that
A1: c in C and
A2: card C = chromatic# G ; :: thesis:
assume A3: for v being Element of Vertices G holds
( not v in c or ex d being Element of C st
( d <> c & ( for w being Element of Vertices G holds
( not w in Adjacent v or not w in d ) ) ) ) ; :: thesis:
set uG = Vertices G;
A4: union C = Vertices G by EQREL_1:def 4;
reconsider c = c as Subset of (Vertices G) by A1;
set Cc = C \ {c};
A6: c in {c} by TARSKI:def 1;

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

consider v being set such that
A8: v in c by A1, XBOOLE_0:def 1;
reconsider v = v as Element of Vertices G by A8;
consider d being Element of C such that
A9: d <> c and
for w being Element of Vertices G 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 set such that
A10: C = {x} by CARD_2:42;
( c = x & d = x ) by A1, A10, TARSKI:def 1;
hence contradiction by A9; :: 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 Vertices G st $1 = vv holds
( $2 <> c & $2 in C & ( for w being Element of Vertices G holds
( not w in Adjacent vv or not w in $2 ) ) );
A11: for e being set st e in c holds
ex u being set st S₁[e,u]

proof

let v be set ; :: thesis:
assume A12: v in c ; :: thesis:
reconsider vv = v as Element of Vertices G by A12;
consider d being Element of C such that
A13: d <> c and
A14: for w being Element of Vertices G holds
( not w in Adjacent vv or not w in d ) by A12, A3;
take d ; :: thesis:
thus S₁[v,d] by A13, A14, A1; :: thesis:

end;

consider r being Function such that
A15: dom r = c and
A16: for e being set st e in c holds
S₁[e,r . e] from CLASSES1:sch 1(A11);
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
A17: d in Cc by XBOOLE_0:def 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 (Vertices G)

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
A20: x = d \/ (r " {d}) ;
A21: r " {d} c= c by A15, RELAT_1:132;
A22: r " {d} c= Vertices G by A21, XBOOLE_1:1;
d in C by XBOOLE_0:def 5;
then x c= Vertices G by A20, A22, XBOOLE_1:8;
hence x in bool (Vertices G) ; :: thesis:

end;

A23: union { H₁(d) where d is Element of Cc : S₂[d] } = Vertices G

proof

thus union { H₁(d) where d is Element of Cc : S₂[d] } c= Vertices G :: 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
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 Vertices G by A24, A25, A19; :: thesis:

end;

thus Vertices G 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 A26: x in Vertices G ; :: thesis:
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 Vertices G by A26;

per cases ;

suppose A29: d = c ; :: thesis:

then r . xp1 <> c by A27, A16;
then A30: not r . xp1 in {c} by TARSKI:def 1;
r . xp1 in C by A27, A29, A16;
then A31: r . xp1 in Cc by A30, 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 A32: 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 A31;
hence x in union { H₁(d) where d is Element of Cc : S₂[d] } by A32, TARSKI:def 4; :: thesis:

end;

suppose d <> c ; :: thesis:

then not d in {c} by TARSKI:def 1;
then d in Cc by A28, XBOOLE_0:def 5;
then A33: 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 A33, TARSKI:def 4; :: thesis:

end;

A34: for A being Subset of (Vertices G) st A in { H₁(d) where d is Element of Cc : S₂[d] } holds
( A <> {} & ( for B being Subset of (Vertices G) 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 (Vertices G); :: thesis:
assume A in { H₁(d) where d is Element of Cc : S₂[d] } ; :: thesis:
then consider da being Element of Cc such that
A35: A = da \/ (r " {da}) ;
A36: da in C by XBOOLE_0:def 5;
hence A <> {} by A35; :: thesis:
let B be Subset of (Vertices G); :: thesis:
assume B in { H₁(d) where d is Element of Cc : S₂[d] } ; :: thesis:
then consider db being Element of Cc such that
A37: B = db \/ (r " {db}) ;
A38: db in C by XBOOLE_0:def 5;

per cases ;

suppose da = db ; :: thesis:

hence ( A = B or A misses B ) by A35, A37; :: thesis:

end;

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

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

per cases by A42, A43, A35, A37, XBOOLE_0:def 3;

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

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

end;

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

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

end;

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

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

end;

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

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

end;

reconsider D = { H₁(d) where d is Element of Cc : S₂[d] } as a_partition of Vertices G by A19, A23, A34, EQREL_1:def 4;

now :: thesis:

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

proof

let a, b be set ; :: according to SCMYCIEL:def 19 :: thesis:
assume that
A58: a <> b and
A56: a in S and
A57: b in S ; :: thesis:
reconsider aa = a, bb = b as Vertex of G by A56, A57;

per cases by A56, A57, A51, XBOOLE_0:def 3;

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

hence not {a,b} in G by A54, A58, Lstable; :: thesis:

end;

suppose that A59: a in d and
A60: b in r " {d} ; :: thesis:

r . b in {d} by A60, FUNCT_1:def 7;
then r . b = d by TARSKI:def 1;
then not a in Adjacent bb by A59, A52, A60, A16;
then not {aa,bb} in Edges G by Ladj;
hence not {a,b} in G by A58, SG4a; :: thesis:

end;

suppose that A61: a in r " {d} and
A62: b in d ; :: thesis:

r . a in {d} by A61, FUNCT_1:def 7;
then r . a = d by TARSKI:def 1;
then not b in Adjacent aa by A62, A52, A61, A16;
then not {bb,aa} in Edges G by Ladj;
hence not {a,b} in G by A58, SG4a; :: thesis:

end;

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

hence not {a,b} in G by A52, A55, A58, Lstable; :: thesis:

end;

hence x is StableSet of G ; :: thesis:

end;

then reconsider D = D as Coloring of G by LStableSetwise;
card Cc = (card C) - (card {c}) by A1, EULER_1:4;
then (card Cc) + 1 = ((card C) - 1) + 1 by CARD_1:30;
then A63: card Cc < card C by NAT_1:13;
deffunc H₂( set ) -> set = $1 \/ (r " {$1});
consider s being Function such that
A64: dom s = Cc and
A65: for x being set st x in Cc holds
s . x = H₂(x) from FUNCT_1:sch 3();
A66: 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
A67: d in dom s and
A68: y = s . d by FUNCT_1:def 3;
y = d \/ (r " {d}) by A64, A65, A67, A68;
hence y in D by A67, A64; :: thesis:

end;

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

proof

let x1, x2 be set ; :: according to FUNCT_1:def 4 :: thesis:
assume that
A70: x1 in dom s and
A71: x2 in dom s and
A72: s . x1 = s . x2 ; :: thesis:
A73: s . x1 = x1 \/ (r " {x1}) by A70, A65, A64;
A74: s . x2 = x2 \/ (r " {x2}) by A71, A65, A64;
thus x1 c= x2 :: according to XBOOLE_0:def 10 :: thesis:

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A75: x in x1 ; :: thesis:
then A76: x in s . x1 by A73, XBOOLE_0:def 3;

per cases by A76, A72, A74, XBOOLE_0:def 3;

suppose x in x2 ; :: thesis:

hence x in x2 ; :: thesis:

end;

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

A78: r " {x2} c= dom r by RELAT_1:132;
A79: x1 in C by A64, A70, XBOOLE_0:def 5;
reconsider x1 = x1 as Subset of (Vertices G) by A64, A70;
x1 meets c by A78, A77, A15, A75, XBOOLE_0:3;
then x1 = c by A79, A1, EQREL_1:def 4;
hence x in x2 by A6, A64, A70, XBOOLE_0:def 5; :: thesis:

end;

thus x2 c= x1 :: thesis:

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A80: x in x2 ; :: thesis:
then A81: x in s . x2 by A74, XBOOLE_0:def 3;

per cases by A81, A72, A73, XBOOLE_0:def 3;

suppose x in x1 ; :: thesis:

hence x in x1 ; :: thesis:

end;

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

A83: r " {x1} c= dom r by RELAT_1:132;
A84: x2 in C by A64, A71, XBOOLE_0:def 5;
reconsider x2 = x2 as Subset of (Vertices G) by A64, A71;
x2 meets c by A83, A82, A15, A80, XBOOLE_0:3;
then x2 = c by A84, A1, EQREL_1:def 4;
hence x in x1 by A6, A64, A71, XBOOLE_0:def 5; :: 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
A85: x = d \/ (r " {d}) ;
s . d = d \/ (r " {d}) by A65;
hence x in rng s by A85, A64, FUNCT_1:def 3; :: thesis:

end;

then D = rng s by A66, XBOOLE_0:def 10;
then s is onto by FUNCT_2:def 3;
then A86: card Cc = card D by A69, A18, EULER_1:11;
then D is finite ;
hence contradiction by A63, A86, A2, Lchro; :: thesis:

end;