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};
A5: c in {c} by TARSKI:def 1;

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

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

end;

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

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

proof

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

end;

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

proof

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

end;

A22: 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 object ; :: 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
A23: x in Y and
A24: Y in { H₁(d) where d is Element of Cc : S₂[d] } by TARSKI:def 4;
thus x in Vertices G by A23, A24, A18; :: thesis:

end;

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A25: x in Vertices G ; :: thesis:
then consider d being set such that
A26: x in d and
A27: d in C by A4, TARSKI:def 4;
reconsider xp1 = x as Element of Vertices G by A25;

per cases ;

suppose A28: d = c ; :: thesis:

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

end;

suppose d <> c ; :: thesis:

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

end;

A33: 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
A34: A = da \/ (r " {da}) ;
A35: da in C by XBOOLE_0:def 5;
hence A <> {} by A34; :: 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
A36: B = db \/ (r " {db}) ;
A37: db in C by XBOOLE_0:def 5;

per cases ;

suppose da = db ; :: thesis:

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

end;

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

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

per cases by A41, A42, A34, A36, XBOOLE_0:def 3;

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

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

end;

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

A45: da <> c by A5, XBOOLE_0:def 5;
r " {db} c= c by A14, RELAT_1:132;
then da meets c by A43, A44, XBOOLE_0:3;
hence contradiction by A45, A35, A1, EQREL_1:def 4; :: thesis:

end;

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

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

end;

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

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

end;

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

now :: thesis:

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

proof

let a, b be set ; :: according to SCMYCIEL:def 19 :: thesis:
assume that
A55: 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, A50, XBOOLE_0:def 3;

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

hence not {a,b} in G by A53, A55, Def19; :: thesis:

end;

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

r . b in {d} by A59, FUNCT_1:def 7;
then A60: r . b = d by TARSKI:def 1;
S₁[b,r . b] by A51, A59, A15;
then not a in Adjacent bb by A58, A60;
then not {aa,bb} in Edges G by Def8;
hence not {a,b} in G by A55, Th12; :: 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 A63: r . a = d by TARSKI:def 1;
S₁[a,r . a] by A51, A61, A15;
then not b in Adjacent aa by A62, A63;
then not {bb,aa} in Edges G by Def8;
hence not {a,b} in G by A55, Th12; :: thesis:

end;

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

hence not {a,b} in G by A51, A54, A55, Def19; :: thesis:

end;

hence x is StableSet of G ; :: thesis:

end;

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

proof

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

end;

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

proof

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A77: x in x1 ; :: thesis:
then A78: x in s . x1 by A74, XBOOLE_0:def 3;

per cases by A78, A73, A75, XBOOLE_0:def 3;

suppose x in x2 ; :: thesis:

hence x in x2 ; :: thesis:

end;

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

A80: r " {x2} c= dom r by RELAT_1:132;
A81: x1 in C by A65, A71, XBOOLE_0:def 5;
reconsider x1 = x1 as Subset of (Vertices G) by A65, A71;
x1 meets c by A80, A79, A14, A77, XBOOLE_0:3;
then x1 = c by A81, A1, EQREL_1:def 4;
hence x in x2 by A5, A65, A71, XBOOLE_0:def 5; :: thesis:

end;

x2 c= x1

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A82: x in x2 ; :: thesis:
then A83: x in s . x2 by A75, XBOOLE_0:def 3;

per cases by A83, A73, A74, XBOOLE_0:def 3;

suppose x in x1 ; :: thesis:

hence x in x1 ; :: thesis:

end;

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

A85: r " {x1} c= dom r by RELAT_1:132;
A86: x2 in C by A65, A72, XBOOLE_0:def 5;
reconsider x2 = x2 as Subset of (Vertices G) by A65, A72;
x2 meets c by A85, A84, A14, A82, XBOOLE_0:3;
then x2 = c by A86, A1, EQREL_1:def 4;
hence x in x1 by A5, A65, A72, XBOOLE_0:def 5; :: thesis:

end;

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

end;

D c= rng s

proof

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

end;

then D = rng s by A67;
then s is onto by FUNCT_2:def 3;
then A88: card Cc = card D by A70, A17, EULER_1:11;
then D is finite ;
hence contradiction by A64, A88, A2, Def22; :: thesis:

end;