let G be finitely_colorable SimpleGraph; :: thesis: ex E being Coloring of (Mycielskian G) st card E = 1 + (chromatic# G)
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]

proof

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

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 ( { (d \/ (r . d)) 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: card { (d \/ (r . d)) where d is Element of C : d in C } = card C

now :: thesis: C is empty

assume not C is empty ; :: thesis: contradiction
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: verum

end;

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

end;

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

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: ( e in C implies ex u being object st S₂[e,u] )
assume e in C ; :: thesis: ex u being object st S₂[e,u]
reconsider A = e as set by TARSKI:1;
take u = A \/ (r . e); :: thesis: S₂[e,u]
thus S₂[e,u] ; :: thesis: verum

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: ( not y in rng s or y in { (d \/ (r . d)) where d is Element of C : d in C } )
assume y in rng s ; :: thesis: y in { (d \/ (r . d)) where d is Element of C : d in C }
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: verum

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: ( not x in { (d \/ (r . d)) where d is Element of C : d in C } or x in rng s )
assume x in { (d \/ (r . d)) where d is Element of C : d in C } ; :: thesis: x in rng s
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: verum

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: ( not x1 in dom s or not x2 in dom s or not s . x1 = s . x2 or x1 = x2 )
assume that
A17: x1 in dom s and
A18: x2 in dom s and
A19: s . x1 = s . x2 ; :: thesis: x1 = x2
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: ( not x in x1 or x in x2 )
assume A23: x in x1 ; :: thesis: x in x2
A24: x in s . x1 by A20, A23, XBOOLE_0:def 3;

per cases ( x in x2 or x in r . x2 ) by A24, A19, A21, XBOOLE_0:def 3;

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

hence x in x2 ; :: thesis: verum

end;

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

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: 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 A27: x in x2 ; :: thesis: x in x1
A28: x in s . x2 by A21, A27, XBOOLE_0:def 3;

per cases ( x in x1 or x in r . x1 ) by A28, A19, A20, XBOOLE_0:def 3;

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

hence x in x1 ; :: thesis: verum

end;

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

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

end;

end;

end;

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

end;

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

end;

end;

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: union (Mycielskian G) c= union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}})

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}}) or x in union (Mycielskian G) )
assume x in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}}) ; :: thesis: x in union (Mycielskian G)
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 ( Y in { (d \/ (r . d)) where d is Element of C : d in C } or Y in {{(union G)}} ) by A34, XBOOLE_0:def 3;

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

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

per cases ( x in d or x in r . d ) by A35, A33, XBOOLE_0:def 3;

suppose A37: x in d ; :: thesis: x in union (Mycielskian G)

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

end;

suppose A39: x in r . d ; :: thesis: x in union (Mycielskian G)

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

end;

end;

end;

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

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

end;

end;

end;

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

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in union (Mycielskian G) or a in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}}) )
assume a in union (Mycielskian G) ; :: thesis: a in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}})
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: a in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}})
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: verum

end;

A48: now :: thesis: for x being set st a = [x,(union G)] & x in union G holds
a in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}})

let x be set ; :: thesis: ( a = [x,(union G)] & x in union G implies a in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}}) )
assume A49: a = [x,(union G)] ; :: thesis: ( x in union G implies a in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}}) )
assume A50: x in union G ; :: thesis: a in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}})
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: verum

end;

per cases ( Y in {{}} or Y in { {x} where x is Element of ((union G) \/ [:(union G),{(union G)}:]) \/ {(union G)} : verum } or Y in Edges G or Y in { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } or Y in { {(union G),[x,(union G)]} where x is Element of union G : x in Vertices G } ) by A43, MYCIELSK:4;

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

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

end;

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

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 ( a in union G or a in [:(union G),{(union G)}:] or a in {(union G)} ) by A57, XBOOLE_0:def 3;

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

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

end;

suppose a in [:(union G),{(union G)}:] ; :: thesis: a in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}})

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

end;

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

{(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: verum

end;

end;

end;

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

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

end;

suppose Y in { {x,[y,(union G)]} where x, y is Element of union G : {x,y} in Edges G } ; :: thesis: a in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}})

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

end;

suppose Y in { {(union G),[x,(union G)]} where x is Element of union G : x in Vertices G } ; :: thesis: a in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}})

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 ( a = union G or a = [x,(union G)] ) by A42, A68, TARSKI:def 2;

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

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

end;

suppose A71: a = [x,(union G)] ; :: thesis: a in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}})

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

end;

end;

end;

end;

end;

end;

A72: now :: thesis: for A being Subset of (union (Mycielskian G)) st A in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}} holds
( A <> {} & ( 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 ) ) )

let A be Subset of (union (Mycielskian G)); :: thesis: ( A in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}} implies ( b₁ <> {} & ( for B being Subset of (union (Mycielskian G)) holds
( not b₂ in { (b₃ \/ (r . b₃)) where d is Element of C : b₃ in C } \/ {{(union G)}} or B = b₂ or B misses b₂ ) ) ) )
assume A73: A in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}} ; :: thesis: ( b₁ <> {} & ( for B being Subset of (union (Mycielskian G)) holds
( not b₂ in { (b₃ \/ (r . b₃)) where d is Element of C : b₃ in C } \/ {{(union G)}} or B = b₂ or B misses b₂ ) ) )

per cases ( A in { (d \/ (r . d)) where d is Element of C : d in C } or A in {{(union G)}} ) by A73, XBOOLE_0:def 3;

suppose A in { (d \/ (r . d)) where d is Element of C : d in C } ; :: thesis: ( b₁ <> {} & ( for B being Subset of (union (Mycielskian G)) holds
( not b₂ in { (b₃ \/ (r . b₃)) where d is Element of C : b₃ in C } \/ {{(union G)}} or B = b₂ or B misses b₂ ) ) )

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: 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 )
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: verum

proof

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

per cases ( B in { (d \/ (r . d)) where d is Element of C : d in C } or B in {{(union G)}} ) by A76, XBOOLE_0:def 3;

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

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

now :: thesis: ( A meets B implies A = B )

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

per cases ( ( x in d & x in e ) or ( x in d & x in r . e ) or ( x in r . d & x in e ) or ( x in r . d & x in r . e ) ) by A79, A80, A77, A74, XBOOLE_0:def 3;

suppose ( x in d & x in e ) ; :: thesis: A = B

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

end;

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

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

end;

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

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

end;

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

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

end;

end;

end;

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

end;

suppose B in {{(union G)}} ; :: thesis: ( A = B or A misses B )

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

now :: thesis: not A meets B

assume A meets B ; :: thesis: contradiction
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 ( union G in d or union G in r . d ) by A93, A91, A74, XBOOLE_0:def 3;

suppose union G in d ; :: thesis: contradiction

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

end;

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

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

end;

end;

end;

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

end;

end;

end;

end;

suppose A96: A in {{(union G)}} ; :: thesis: ( b₁ <> {} & ( for B being Subset of (union (Mycielskian G)) holds
( not b₂ in { (b₃ \/ (r . b₃)) where d is Element of C : b₃ in C } \/ {{(union G)}} or B = b₂ or B misses b₂ ) ) )

then A97: A = {(union G)} by TARSKI:def 1;
thus A <> {} by A96; :: thesis: 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 )
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: verum

proof

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

per cases ( B in { (d \/ (r . d)) where d is Element of C : d in C } or B in {{(union G)}} ) by A98, XBOOLE_0:def 3;

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

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

now :: thesis: not A meets B

assume A meets B ; :: thesis: contradiction
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 ( union G in d or union G in r . d ) by A103, A102, A99, XBOOLE_0:def 3;

suppose union G in d ; :: thesis: contradiction

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

end;

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

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

end;

end;

end;

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

end;

suppose B in {{(union G)}} ; :: thesis: ( A = B or A misses B )

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

end;

end;

end;

end;

end;

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: ( not x in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}} or x in bool (union (Mycielskian G)) )
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: x in bool (union (Mycielskian G))

per cases ( x in { (d \/ (r . d)) where d is Element of C : d in C } or x in {{(union G)}} ) by A107, XBOOLE_0:def 3;

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

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: ( not y in r . d or y in union (Mycielskian G) )
assume A112: y in r . d ; :: thesis: y in union (Mycielskian G)
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: verum

end;

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

end;

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

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

end;

end;

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: ( e in E implies e is StableSet of (Mycielskian G) )
assume A116: e in E ; :: thesis: e is StableSet of (Mycielskian G)
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: ( x <> y & x in e1 & y in e1 implies {x,y} nin Mycielskian G )
assume that
A117: x <> y and
A118: x in e1 and
A119: y in e1 ; :: thesis: {x,y} nin Mycielskian G

per cases ( e in { (d \/ (r . d)) where d is Element of C : d in C } or e in {{(union G)}} ) by A116, XBOOLE_0:def 3;

suppose e in { (d \/ (r . d)) where d is Element of C : d in C } ; :: thesis: {x,y} nin Mycielskian G

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 ( ( x in d & y in d ) or ( x in d & y in r . d ) or ( x in r . d & y in d ) or ( x in r . d & y in r . d ) ) by A120, A118, A119, XBOOLE_0:def 3;

suppose A124: ( x in d & y in d ) ; :: thesis: {x,y} nin Mycielskian G

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

end;

suppose that A125: x in d and
A126: y in r . d ; :: thesis: {x,y} nin Mycielskian G

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

per cases ( x1 = x or x1 <> x ) ;

suppose x1 = x ; :: thesis: {x,y} nin Mycielskian G

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

end;

suppose x1 <> x ; :: thesis: {x,y} nin Mycielskian G

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

end;

end;

end;

suppose that A129: x in r . d and
A130: y in d ; :: thesis: {x,y} nin Mycielskian G

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

per cases ( x1 = y or x1 <> y ) ;

suppose x1 = y ; :: thesis: {x,y} nin Mycielskian G

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

end;

suppose x1 <> y ; :: thesis: {x,y} nin Mycielskian G

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

end;

end;

end;

suppose that A133: x in r . d and
A134: y in r . d ; :: thesis: {x,y} nin Mycielskian G

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

end;

end;

end;

suppose e in {{(union G)}} ; :: thesis: {x,y} nin Mycielskian G

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

end;

end;

end;

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

end;

then reconsider E = E as Coloring of (Mycielskian G) ;
take E ; :: thesis: card E = 1 + (chromatic# G)

now :: thesis: not {(union G)} in { (d \/ (r . d)) where d is Element of C : d in C }

assume {(union G)} in { (d \/ (r . d)) where d is Element of C : d in C } ; :: thesis: contradiction
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 ( union G in d or union G in r . d ) by A139, XBOOLE_0:def 3;

suppose union G in d ; :: thesis: contradiction

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

end;

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

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

end;

end;

end;

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