let G be finitely_colorable SimpleGraph; :: thesis:
set uG = union G;
set MG = Mycielskian G;
set uMG = union (Mycielskian G);
set cnG = chromatic# G;
consider C being finite Coloring of G such that
A1: card C = chromatic# G by Def22;
defpred S₁[ object , object ] means ex A being set st
( A = $1 & $2 = { [x,(union G)] where x is Element of union G : x in A } );
A2: for e being object st e in C holds
ex u being object st S₁[e,u]

let e be object ; :: thesis:
assume e in C ; :: thesis:
reconsider A = e as set by TARSKI:1;
take u = { [x,(union G)] where x is Element of union G : x in A } ; :: thesis:
thus S₁[e,u] ; :: thesis:

end;

consider r being Function such that
dom r = C and
A3: for e being object st e in C holds
S₁[e,r . e] from CLASSES1:sch 1(A2);
set D = { (d \/ (r . d)) where d is Element of C : d in C } ;
A4: card { (d \/ (r . d)) where d is Element of C : d in C } = card C

proof

per cases ) where d is Element of C : d in C } is empty or not { (d \/ (r . d)) where d is Element of C : d in C } is empty ) ;

suppose A5: { (d \/ (r . d)) where d is Element of C : d in C } is empty ; :: thesis:

now :: thesis:

assume not C is empty ; :: thesis:
then consider c being object such that
A6: c in C ;
reconsider c = c as set by TARSKI:1;
c \/ (r . c) in { (d \/ (r . d)) where d is Element of C : d in C } by A6;
hence contradiction by A5; :: thesis:

end;

hence card { (d \/ (r . d)) where d is Element of C : d in C } = card C by A5; :: thesis:

end;

suppose A7: not { (d \/ (r . d)) where d is Element of C : d in C } is empty ; :: thesis:

defpred S₂[ object , object ] means ex A being set st
( A = $1 & $2 = A \/ (r . $1) );
A8: for e being object st e in C holds
ex u being object st S₂[e,u]

proof

let e be object ; :: thesis:
assume e in C ; :: thesis:
reconsider A = e as set by TARSKI:1;
take u = A \/ (r . e); :: thesis:
thus S₂[e,u] ; :: thesis:

end;

consider s being Function such that
A9: dom s = C and
A10: for e being object st e in C holds
S₂[e,s . e] from CLASSES1:sch 1(A8);
A11: rng s c= { (d \/ (r . d)) where d is Element of C : d in C }

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng s ; :: thesis:
then consider x being object such that
A12: x in dom s and
A13: y = s . x by FUNCT_1:def 3;
reconsider x = x as set by TARSKI:1;
S₂[x,y] by A12, A13, A9, A10;
then y = x \/ (r . x) ;
hence y in { (d \/ (r . d)) where d is Element of C : d in C } by A12, A9; :: thesis:

end;

then reconsider s = s as Function of C, { (d \/ (r . d)) where d is Element of C : d in C } by A9, FUNCT_2:2;
{ (d \/ (r . d)) where d is Element of C : d in C } c= rng s

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { (d \/ (r . d)) where d is Element of C : d in C } ; :: thesis:
then consider c being Element of C such that
A14: x = c \/ (r . c) and
A15: c in C ;
S₂[c,s . c] by A15, A10;
then x = s . c by A14;
hence x in rng s by A15, A9, FUNCT_1:def 3; :: thesis:

end;

then rng s = { (d \/ (r . d)) where d is Element of C : d in C } by A11;
then A16: s is onto by FUNCT_2:def 3;
s is one-to-one

proof

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis:
assume that
A17: x1 in dom s and
A18: x2 in dom s and
A19: s . x1 = s . x2 ; :: thesis:
reconsider x1 = x1, x2 = x2 as set by TARSKI:1;
S₂[x1,s . x1] by A17, A9, A10;
then A20: s . x1 = x1 \/ (r . x1) ;
S₂[x2,s . x2] by A18, A9, A10;
then A21: s . x2 = x2 \/ (r . x2) ;
A22: x1 c= x2

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A23: x in x1 ; :: thesis:
A24: x in s . x1 by A20, A23, XBOOLE_0:def 3;

per cases by A24, A19, A21, XBOOLE_0:def 3;

suppose x in x2 ; :: thesis:

hence x in x2 ; :: thesis:

end;

suppose A25: x in r . x2 ; :: thesis:

S₁[x2,r . x2] by A3, A9, A18;
then x in { [xx,(union G)] where xx is Element of union G : xx in x2 } by A25;
then consider xx being Element of union G such that
A26: x = [xx,(union G)] and
xx in x2 ;
thus x in x2 by A26, A17, A23, A9, Th1; :: thesis:

end;

x2 c= x1

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A27: x in x2 ; :: thesis:
A28: x in s . x2 by A21, A27, XBOOLE_0:def 3;

per cases by A28, A19, A20, XBOOLE_0:def 3;

suppose x in x1 ; :: thesis:

hence x in x1 ; :: thesis:

end;

suppose A29: x in r . x1 ; :: thesis:

S₁[x1,r . x1] by A3, A9, A17;
then x in { [xx,(union G)] where xx is Element of union G : xx in x1 } by A29;
then consider xx being Element of union G such that
A30: x = [xx,(union G)] and
xx in x1 ;
thus x in x1 by A30, A18, A27, A9, Th1; :: thesis:

end;

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

end;

hence card { (d \/ (r . d)) where d is Element of C : d in C } = card C by A16, A7, EULER_1:11; :: thesis:

end;

A31: { (d \/ (r . d)) where d is Element of C : d in C } is finite by A4;
set E = { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}};
A32: union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}}) = union (Mycielskian G)

proof

thus union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}}) c= union (Mycielskian G) :: according to XBOOLE_0:def 10 :: thesis:

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}}) ; :: thesis:
then consider Y being set such that
A33: x in Y and
A34: Y in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}} by TARSKI:def 4;

per cases by A34, XBOOLE_0:def 3;

suppose Y in { (d \/ (r . d)) where d is Element of C : d in C } ; :: thesis:

then consider d being Element of C such that
A35: Y = d \/ (r . d) and
A36: d in C ;

per cases by A35, A33, XBOOLE_0:def 3;

suppose A37: x in d ; :: thesis:

A38: union G c= union (Mycielskian G) by Th84, ZFMISC_1:77;
x in union G by A37;
hence x in union (Mycielskian G) by A38; :: thesis:

end;

suppose A39: x in r . d ; :: thesis:

S₁[d,r . d] by A3, A36;
then x in { [yy,(union G)] where yy is Element of union G : yy in d } by A39;
then consider yy being Element of union G such that
A40: x = [yy,(union G)] and
A41: yy in d ;
{x} in Mycielskian G by A40, A41, Th95;
hence x in union (Mycielskian G) by Th24; :: thesis:

end;

suppose Y in {{(union G)}} ; :: thesis:

then Y = {(union G)} by TARSKI:def 1;
then x = union G by A33, TARSKI:def 1;
hence x in union (Mycielskian G) by Th87; :: thesis:

end;

thus union (Mycielskian G) c= union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}}) :: thesis:

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in union (Mycielskian G) ; :: thesis:
then consider Y being set such that
A42: a in Y and
A43: Y in Mycielskian G by TARSKI:def 4;
A44: ( a in union G implies a in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}}) )

proof

assume a in union G ; :: thesis:
then a in union C by EQREL_1:def 4;
then consider d being set such that
A45: a in d and
A46: d in C by TARSKI:def 4;
A47: a in d \/ (r . d) by A45, XBOOLE_0:def 3;
d \/ (r . d) in { (d \/ (r . d)) where d is Element of C : d in C } by A46;
then d \/ (r . d) in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}} by XBOOLE_0:def 3;
hence a in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}}) by A47, TARSKI:def 4; :: thesis:

end;

A48: now :: thesis:

let x be set ; :: thesis:
assume A49: a = [x,(union G)] ; :: thesis:
assume A50: x in union G ; :: thesis:
then x in union C by EQREL_1:def 4;
then consider d being set such that
A51: x in d and
A52: d in C by TARSKI:def 4;
d \/ (r . d) in { (d \/ (r . d)) where d is Element of C : d in C } by A52;
then A53: d \/ (r . d) in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}} by XBOOLE_0:def 3;
A54: a in { [xx,(union G)] where xx is Element of union G : xx in d } by A51, A49, A50;
S₁[d,r . d] by A3, A52;
then a in r . d by A54;
then a in d \/ (r . d) by XBOOLE_0:def 3;
hence a in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}}) by A53, TARSKI:def 4; :: thesis:

end;

per cases by A43, MYCIELSK:4;

suppose Y in {{}} ; :: thesis:

hence a in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}}) by A42, TARSKI:def 1; :: thesis:

end;

suppose Y in { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } ; :: thesis:

then consider x being Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} such that
A55: Y = {x} ;
A56: a = x by A55, A42, TARSKI:def 1;
A57: ( a in (union G) \/ [:(union G),{(union G)}:] or a in {(union G)} ) by A56, XBOOLE_0:def 3;

per cases by A57, XBOOLE_0:def 3;

suppose a in union G ; :: thesis:

hence a in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}}) by A44; :: thesis:

end;

suppose a in [:(union G),{(union G)}:] ; :: thesis:

then consider x, y being object such that
A58: x in union G and
A59: y in {(union G)} and
A60: a = [x,y] by ZFMISC_1:def 2;
y = union G by A59, TARSKI:def 1;
hence a in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}}) by A58, A60, A48; :: thesis:

end;

suppose A61: a in {(union G)} ; :: thesis:

{(union G)} in {{(union G)}} by TARSKI:def 1;
then {(union G)} in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}} by XBOOLE_0:def 3;
hence a in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}}) by A61, TARSKI:def 4; :: thesis:

end;

suppose Y in Edges G ; :: thesis:

then consider p, r being set such that
p <> r and
A62: p in Vertices G and
A63: r in Vertices G and
A64: Y = {p,r} by Th11;
thus a in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}}) by A44, A62, A63, A64, A42, TARSKI:def 2; :: thesis:

end;

suppose Y in { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } ; :: thesis:

then consider x, y being Element of union G such that
A65: Y = {x,[y,(union G)]} and
A66: {x,y} in Edges G ;
A67: ( a = x or a = [y,(union G)] ) by A42, A65, TARSKI:def 2;
x in union G by A66, Th13;
hence a in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}}) by A67, A44, A48; :: thesis:

end;

suppose Y in { {(union G),[x,(union G)]} where x is Element of union G : x in Vertices G } ; :: thesis:

then consider x being Element of union G such that
A68: Y = {(union G),[x,(union G)]} and
A69: x in Vertices G ;

per cases by A42, A68, TARSKI:def 2;

suppose a = union G ; :: thesis:

then A70: a in {(union G)} by TARSKI:def 1;
{(union G)} in {{(union G)}} by TARSKI:def 1;
then {(union G)} in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}} by XBOOLE_0:def 3;
hence a in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}}) by A70, TARSKI:def 4; :: thesis:

end;

suppose A71: a = [x,(union G)] ; :: thesis:

thus a in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}}) by A71, A48, A69; :: thesis:

end;

A72: now :: thesis:

let A be Subset of (union (Mycielskian G)); :: thesis:
assume A73: A in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}} ; :: thesis:

per cases by A73, XBOOLE_0:def 3;

suppose A in { (d \/ (r . d)) where d is Element of C : d in C } ; :: thesis:

then consider d being Element of C such that
A74: A = d \/ (r . d) and
A75: d in C ;
thus A <> {} by A74, A75; :: thesis:
thus for B being Subset of (union (Mycielskian G)) holds
( not B in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}} or A = B or A misses B ) :: thesis:

proof

let B be Subset of (union (Mycielskian G)); :: thesis:
assume A76: B in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}} ; :: thesis:

per cases by A76, XBOOLE_0:def 3;

suppose B in { (d \/ (r . d)) where d is Element of C : d in C } ; :: thesis:

then consider e being Element of C such that
A77: B = e \/ (r . e) and
A78: e in C ;

now :: thesis:

assume A meets B ; :: thesis:
then consider x being object such that
A79: x in A and
A80: x in B by XBOOLE_0:3;

per cases by A79, A80, A77, A74, XBOOLE_0:def 3;

suppose ( x in d & x in e ) ; :: thesis:

then d = e by EQREL_1:70;
hence A = B by A77, A74; :: thesis:

end;

suppose A81: ( x in d & x in r . e ) ; :: thesis:

then S₁[e,r . e] by A3;
then x in { [yy,(union G)] where yy is Element of union G : yy in e } by A81;
then consider yy being Element of union G such that
A82: x = [yy,(union G)] and
yy in e ;
thus A = B by A82, Th1, A81; :: thesis:

end;

suppose A83: ( x in r . d & x in e ) ; :: thesis:

then S₁[d,r . d] by A3;
then x in { [yy,(union G)] where yy is Element of union G : yy in d } by A83;
then consider yy being Element of union G such that
A84: x = [yy,(union G)] and
yy in d ;
thus A = B by A84, Th1, A83; :: thesis:

end;

suppose A85: ( x in r . d & x in r . e ) ; :: thesis:

S₁[d,r . d] by A3, A75;
then x in { [yy,(union G)] where yy is Element of union G : yy in d } by A85;
then consider yy being Element of union G such that
A86: x = [yy,(union G)] and
A87: yy in d ;
S₁[e,r . e] by A3, A78;
then x in { [zz,(union G)] where zz is Element of union G : zz in e } by A85;
then consider zz being Element of union G such that
A88: x = [zz,(union G)] and
A89: zz in e ;
yy = zz by A86, A88, XTUPLE_0:1;
then d = e by A87, A89, EQREL_1:70;
hence A = B by A77, A74; :: thesis:

end;

hence ( A = B or A misses B ) ; :: thesis:

end;

suppose B in {{(union G)}} ; :: thesis:

then A90: B = {(union G)} by TARSKI:def 1;

now :: thesis:

assume A meets B ; :: thesis:
then consider x being object such that
A91: x in A and
A92: x in B by XBOOLE_0:3;
A93: x = union G by A92, A90, TARSKI:def 1;

per cases by A93, A91, A74, XBOOLE_0:def 3;

suppose union G in d ; :: thesis:

then union G in union G ;
hence contradiction ; :: thesis:

end;

suppose A94: union G in r . d ; :: thesis:

S₁[d,r . d] by A3, A75;
then union G in { [yy,(union G)] where yy is Element of union G : yy in d } by A94;
then consider yy being Element of union G such that
A95: union G = [yy,(union G)] and
yy in d ;
thus contradiction by A95, Th2; :: thesis:

end;

hence ( A = B or A misses B ) ; :: thesis:

end;

suppose A96: A in {{(union G)}} ; :: thesis:

then A97: A = {(union G)} by TARSKI:def 1;
thus A <> {} by A96; :: thesis:
thus for B being Subset of (union (Mycielskian G)) holds
( not B in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}} or A = B or A misses B ) :: thesis:

proof

let B be Subset of (union (Mycielskian G)); :: thesis:
assume A98: B in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}} ; :: thesis:

per cases by A98, XBOOLE_0:def 3;

suppose B in { (d \/ (r . d)) where d is Element of C : d in C } ; :: thesis:

then consider d being Element of C such that
A99: B = d \/ (r . d) and
A100: d in C ;

now :: thesis:

assume A meets B ; :: thesis:
then consider x being object such that
A101: x in A and
A102: x in B by XBOOLE_0:3;
A103: x = union G by A101, A97, TARSKI:def 1;

per cases by A103, A102, A99, XBOOLE_0:def 3;

suppose union G in d ; :: thesis:

then union G in union G ;
hence contradiction ; :: thesis:

end;

suppose A104: union G in r . d ; :: thesis:

S₁[d,r . d] by A3, A100;
then union G in { [yy,(union G)] where yy is Element of union G : yy in d } by A104;
then consider yy being Element of union G such that
A105: union G = [yy,(union G)] and
yy in d ;
thus contradiction by A105, Th2; :: thesis:

end;

hence ( A = B or A misses B ) ; :: thesis:

end;

suppose B in {{(union G)}} ; :: thesis:

hence ( A = B or A misses B ) by A97, TARSKI:def 1; :: thesis:

end;

A106: { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}} c= bool (union (Mycielskian G))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
reconsider x1 = x as set by TARSKI:1;
assume A107: x in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}} ; :: thesis:

per cases by A107, XBOOLE_0:def 3;

suppose x in { (d \/ (r . d)) where d is Element of C : d in C } ; :: thesis:

then consider d being Element of C such that
A108: x = d \/ (r . d) and
A109: d in C ;
A110: union G c= union (Mycielskian G) by Th84, ZFMISC_1:77;
A111: d c= union (Mycielskian G) by A110;
r . d c= union (Mycielskian G)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A112: y in r . d ; :: thesis:
S₁[d,r . d] by A3, A109;
then y in { [yy,(union G)] where yy is Element of union G : yy in d } by A112;
then consider yy being Element of union G such that
A113: y = [yy,(union G)] and
A114: yy in d ;
{y} in Mycielskian G by A113, A114, Th95;
hence y in union (Mycielskian G) by Th24; :: thesis:

end;

then x1 c= union (Mycielskian G) by A108, A111, XBOOLE_1:8;
hence x in bool (union (Mycielskian G)) ; :: thesis:

end;

suppose x in {{(union G)}} ; :: thesis:

then A115: x = {(union G)} by TARSKI:def 1;
union G in union (Mycielskian G) by Th87;
then x1 c= union (Mycielskian G) by A115, ZFMISC_1:31;
hence x in bool (union (Mycielskian G)) ; :: thesis:

end;

reconsider E = { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}} as a_partition of union (Mycielskian G) by A32, A72, A106, EQREL_1:def 4;
E is StableSet-wise

proof

let e be set ; :: according to SCMYCIEL:def 20 :: thesis:
assume A116: e in E ; :: thesis:
reconsider e1 = e as Subset of (union (Mycielskian G)) by A116;
e1 is stable

proof

let x, y be set ; :: according to SCMYCIEL:def 19 :: thesis:
assume that
A117: x <> y and
A118: x in e1 and
A119: y in e1 ; :: thesis:

per cases by A116, XBOOLE_0:def 3;

suppose e in { (d \/ (r . d)) where d is Element of C : d in C } ; :: thesis:

then consider d being Element of C such that
A120: e = d \/ (r . d) and
A121: d in C ;
A122: S₁[d,r . d] by A3, A121;
A123: d is stable by Def20;

per cases by A120, A118, A119, XBOOLE_0:def 3;

suppose A124: ( x in d & y in d ) ; :: thesis:

then {x,y} nin G by A123, A117;
hence {x,y} nin Mycielskian G by A124, Th103; :: thesis:

end;

suppose that A125: x in d and
A126: y in r . d ; :: thesis:

consider x1 being Element of union G such that
A127: y = [x1,(union G)] and
A128: x1 in d by A126, A122;

per cases ;

suppose x1 = x ; :: thesis:

hence {x,y} nin Mycielskian G by A127, Th100; :: thesis:

end;

suppose x1 <> x ; :: thesis:

then {x1,x} nin G by A125, A128, A123;
hence {x,y} nin Mycielskian G by A125, A127, Th101; :: thesis:

end;

suppose that A129: x in r . d and
A130: y in d ; :: thesis:

consider x1 being Element of union G such that
A131: x = [x1,(union G)] and
A132: x1 in d by A129, A122;

per cases ;

suppose x1 = y ; :: thesis:

hence {x,y} nin Mycielskian G by A131, Th100; :: thesis:

end;

suppose x1 <> y ; :: thesis:

then {x1,y} nin G by A130, A132, A123;
hence {x,y} nin Mycielskian G by A131, A130, Th101; :: thesis:

end;

suppose that A133: x in r . d and
A134: y in r . d ; :: thesis:

consider x1 being Element of union G such that
A135: x = [x1,(union G)] and
x1 in d by A133, A122;
consider y1 being Element of union G such that
A136: y = [y1,(union G)] and
y1 in d by A134, A122;
thus {x,y} nin Mycielskian G by A135, A136, A117, Th98; :: thesis:

end;

suppose e in {{(union G)}} ; :: thesis:

then e = {(union G)} by TARSKI:def 1;
then ( x = union G & y = union G ) by A118, A119, TARSKI:def 1;
hence {x,y} nin Mycielskian G by A117; :: thesis:

end;

hence e is StableSet of (Mycielskian G) ; :: thesis:

end;

then reconsider E = E as Coloring of (Mycielskian G) ;
take E ; :: thesis:

now :: thesis:

assume {(union G)} in { (d \/ (r . d)) where d is Element of C : d in C } ; :: thesis:
then consider d being Element of C such that
A137: {(union G)} = d \/ (r . d) and
A138: d in C ;
A139: union G in d \/ (r . d) by A137, TARSKI:def 1;

per cases by A139, XBOOLE_0:def 3;

suppose union G in d ; :: thesis:

then union G in union G ;
hence contradiction ; :: thesis:

end;

suppose A140: union G in r . d ; :: thesis:

S₁[d,r . d] by A3, A138;
then union G in { [x,(union G)] where x is Element of union G : x in d } by A140;
then consider x being Element of union G such that
A141: union G = [x,(union G)] and
x in d ;
thus contradiction by A141, Th2; :: thesis:

end;

hence card E = 1 + (chromatic# G) by A4, A31, A1, CARD_2:41; :: thesis: