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
A: card C = chromatic# G by Lchro;
defpred S₁[ set , set ] means $2 = { [x,(union G)] where x is Element of union G : x in $1 } ;
P: for e being set st e in C holds
ex u being set st S₁[e,u] ;
consider r being Function such that
dom r = C and
C: for e being set st e in C holds
S₁[e,r . e] from CLASSES1:sch 1(P);
set D = { (d \/ (r . d)) where d is Element of C : d in C } ;
D1: 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 A7: { (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 set such that
A8: c in C by XBOOLE_0:def 1;
c \/ (r . c) in { (d \/ (r . d)) where d is Element of C : d in C } by A8;
hence contradiction by A7; :: thesis: verum

end;

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

end;

suppose A9: 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₂[ set , set ] means $2 = $1 \/ (r . $1);
A10: for e being set st e in C holds
ex u being set st S₂[e,u] ;
consider s being Function such that
A11: dom s = C and
A12: for e being set st e in C holds
S₂[e,s . e] from CLASSES1:sch 1(A10);
A13: rng s c= { (d \/ (r . d)) where d is Element of C : d in C }

proof

let y be set ; :: 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 set such that
A14: x in dom s and
A15: y = s . x by FUNCT_1:def 3;
y = x \/ (r . x) by A14, A15, A11, A12;
hence y in { (d \/ (r . d)) where d is Element of C : d in C } by A14, A11; :: thesis: verum

end;

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

proof

let x be set ; :: 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
A16: x = c \/ (r . c) and
A17: c in C ;
x = s . c by A16, A17, A12;
hence x in rng s by A17, A11, FUNCT_1:def 3; :: thesis: verum

end;

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

proof

let x1, x2 be set ; :: 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
A19: x1 in dom s and
A20: x2 in dom s and
A21: s . x1 = s . x2 ; :: thesis: x1 = x2
A22: s . x1 = x1 \/ (r . x1) by A19, A11, A12;
A23: s . x2 = x2 \/ (r . x2) by A20, A11, A12;
thus x1 c= x2 :: according to XBOOLE_0:def 10 :: thesis: x2 c= x1

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in x1 or x in x2 )
assume A24: x in x1 ; :: thesis: x in x2
A25: x in s . x1 by A22, A24, XBOOLE_0:def 3;

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

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

hence x in x2 ; :: thesis: verum

end;

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

then x in { [xx,(union G)] where xx is Element of union G : xx in x2 } by C, A11, A20;
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, A19, A24, A11, Aux1; :: thesis: verum

end;

end;

end;

thus x2 c= x1 :: thesis: verum

proof

let x be set ; :: 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 A23, A27, XBOOLE_0:def 3;

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

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

hence x in x1 ; :: thesis: verum

end;

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

then x in { [xx,(union G)] where xx is Element of union G : xx in x1 } by C, A11, A19;
then consider xx being Element of union G such that
A26: x = [xx,(union G)] and
xx in x1 ;
thus x in x1 by A26, A20, A27, A11, Aux1; :: thesis: verum

end;

end;

end;

end;

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

end;

end;

end;

D1a: { (d \/ (r . d)) where d is Element of C : d in C } is finite by D1;
set E = { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}};
E1: 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 set ; :: 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
A2: x in Y and
B2: 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 B2, 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
A3: Y = d \/ (r . d) and
B3: d in C ;

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

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

B4: union G c= union (Mycielskian G) by M0, ZFMISC_1:77;
x in union G by S3;
hence x in union (Mycielskian G) by B4; :: thesis: verum

end;

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

then x in { [yy,(union G)] where yy is Element of union G : yy in d } by B3, C;
then consider yy being Element of union G such that
A8: x = [yy,(union G)] and
B8: yy in d ;
{x} in Mycielskian G by A8, B8, M0e2aa;
hence x in union (Mycielskian G) by Vertices0; :: 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 A2, TARSKI:def 1;
hence x in union (Mycielskian G) by M00; :: 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 set ; :: 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
A2: a in Y and
B2: Y in Mycielskian G by TARSKI:def 4;
C2: ( 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
D4: a in d and
E4: d in C by TARSKI:def 4;
F4: a in d \/ (r . d) by D4, XBOOLE_0:def 3;
d \/ (r . d) in { (d \/ (r . d)) where d is Element of C : d in C } by E4;
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 F4, TARSKI:def 4; :: thesis: verum

end;

D2: 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 A4: 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 B4: 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
D4: x in d and
E4: d in C by TARSKI:def 4;
d \/ (r . d) in { (d \/ (r . d)) where d is Element of C : d in C } by E4;
then G4: d \/ (r . d) in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}} by XBOOLE_0:def 3;
a in { [xx,(union G)] where xx is Element of union G : xx in d } by D4, A4, B4;
then a in r . d by E4, C;
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 G4, 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 B2, 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 A2, 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
A3: Y = {x} and
verum ;
C3: a = x by A3, A2, TARSKI:def 1;
D3: ( a in (union G) \/ [:(union G),{(union G)}:] or a in {(union G)} ) by C3, XBOOLE_0:def 3;

per cases ( a in union G or a in [:(union G),{(union G)}:] or a in {(union G)} ) by D3, 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 C2; :: 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 set such that
A4: x in union G and
B4: y in {(union G)} and
C4: a = [x,y] by ZFMISC_1:def 2;
y = union G by B4, TARSKI:def 1;
hence a in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}}) by A4, C4, D2; :: thesis: verum

end;

suppose S4: 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 S4, 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
B3: p in Vertices G and
C3: r in Vertices G and
D3: Y = {p,r} by SG4;
thus a in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}}) by C2, B3, C3, D3, A2, 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
A3: Y = {x,[y,(union G)]} and
B3: {x,y} in Edges G ;
C3: ( a = x or a = [y,(union G)] ) by A2, A3, TARSKI:def 2;
x in union G by B3, SG5;
hence a in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(union G)}}) by C3, C2, D2; :: 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
A3: Y = {(union G),[x,(union G)]} and
B3: x in Vertices G ;

per cases ( a = union G or a = [x,(union G)] ) by A2, A3, 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 A4: 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 A4, TARSKI:def 4; :: thesis: verum

end;

suppose A4: 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 A4, D2, B3; :: thesis: verum

end;

end;

end;

end;

end;

end;

F1: 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 A2: 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 A2, 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
A3: A = d \/ (r . d) and
B3: d in C ;
thus A <> {} by A3, B3; :: 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 A4: 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 A4, 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
A5: B = e \/ (r . e) and
B5: e in C ;

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

assume A meets B ; :: thesis: A = B
then consider x being set such that
A6: x in A and
B6: 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 A6, B6, A5, A3, 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 A5, A3; :: thesis: verum

end;

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

x in { [yy,(union G)] where yy is Element of union G : yy in e } by A7, C;
then consider yy being Element of union G such that
A8: x = [yy,(union G)] and
yy in e ;
thus A = B by A8, Aux1, A7; :: thesis: verum

end;

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

x in { [yy,(union G)] where yy is Element of union G : yy in d } by A7, C;
then consider yy being Element of union G such that
A8: x = [yy,(union G)] and
yy in d ;
thus A = B by A8, Aux1, A7; :: thesis: verum

end;

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

x in { [yy,(union G)] where yy is Element of union G : yy in d } by A7, B3, C;
then consider yy being Element of union G such that
A8: x = [yy,(union G)] and
B8: yy in d ;
x in { [zz,(union G)] where zz is Element of union G : zz in e } by A7, B5, C;
then consider zz being Element of union G such that
C8: x = [zz,(union G)] and
D8: zz in e ;
yy = zz by A8, C8, XTUPLE_0:1;
then d = e by B8, D8, EQREL_1:70;
hence A = B by A5, A3; :: 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 B5: B = {(union G)} by TARSKI:def 1;

now :: thesis: not A meets B

assume A meets B ; :: thesis: contradiction
then consider x being set such that
A4: x in A and
B4: x in B by XBOOLE_0:3;
C4: x = union G by B4, B5, TARSKI:def 1;

per cases ( union G in d or union G in r . d ) by C4, A4, A3, XBOOLE_0:def 3;

suppose union G in d ; :: thesis: contradiction

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

end;

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

then union G in { [yy,(union G)] where yy is Element of union G : yy in d } by B3, C;
then consider yy being Element of union G such that
A4: union G = [yy,(union G)] and
yy in d ;
thus contradiction by A4, Aux2; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

end;

suppose A2a: 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 A2: A = {(union G)} by TARSKI:def 1;
thus A <> {} by A2a; :: 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 B2: 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 B2, 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
A3: B = d \/ (r . d) and
B3: d in C ;

now :: thesis: not A meets B

assume A meets B ; :: thesis: contradiction
then consider x being set such that
A4: x in A and
B4: x in B by XBOOLE_0:3;
C4: x = union G by A4, A2, TARSKI:def 1;

per cases ( union G in d or union G in r . d ) by C4, B4, A3, XBOOLE_0:def 3;

suppose union G in d ; :: thesis: contradiction

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

end;

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

then union G in { [yy,(union G)] where yy is Element of union G : yy in d } by B3, C;
then consider yy being Element of union G such that
A4: union G = [yy,(union G)] and
yy in d ;
thus contradiction by A4, Aux2; :: 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 A2, TARSKI:def 1; :: thesis: verum

end;

end;

end;

end;

end;

end;

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

proof

let x be set ; :: 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)) )
assume A2: 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 A2, 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
A3: x = d \/ (r . d) and
B3: d in C ;
E3: union G c= union (Mycielskian G) by M0, ZFMISC_1:77;
C3: d c= union (Mycielskian G) by E3, XBOOLE_1:1;
r . d c= union (Mycielskian G)

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in r . d or y in union (Mycielskian G) )
assume y in r . d ; :: thesis: y in union (Mycielskian G)
then y in { [yy,(union G)] where yy is Element of union G : yy in d } by B3, C;
then consider yy being Element of union G such that
A4: y = [yy,(union G)] and
B4: yy in d ;
{y} in Mycielskian G by A4, B4, M0e2aa;
hence y in union (Mycielskian G) by Vertices0; :: thesis: verum

end;

then x c= union (Mycielskian G) by A3, C3, 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 A3: x = {(union G)} by TARSKI:def 1;
union G in union (Mycielskian G) by M00;
then x c= union (Mycielskian G) by A3, 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 E1, F1, G1, 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 A1: e in E ; :: thesis: e is StableSet of (Mycielskian G)
reconsider e1 = e as Subset of (union (Mycielskian G)) by A1;
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
A2: x <> y and
B2: x in e1 and
C2: 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 A1, 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
A3: e = d \/ (r . d) and
B3: d in C ;
C3: S₁[d,r . d] by C, B3;
D3: d is stable by B3, LStableSetwise;

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 A3, B2, C2, XBOOLE_0:def 3;

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

then {x,y} nin G by D3, A2, Lstable;
hence {x,y} nin Mycielskian G by S3, M1; :: thesis: verum

end;

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

consider x1 being Element of union G such that
A4: y = [x1,(union G)] and
B4: x1 in d by S3b, C3;

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

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

hence {x,y} nin Mycielskian G by A4, M0e4a; :: thesis: verum

end;

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

then {x1,x} nin G by S3a, B4, D3, Lstable;
hence {x,y} nin Mycielskian G by S3a, A4, M0e4b; :: thesis: verum

end;

end;

end;

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

consider x1 being Element of union G such that
A4: x = [x1,(union G)] and
B4: x1 in d by S3a, C3;

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

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

hence {x,y} nin Mycielskian G by A4, M0e4a; :: thesis: verum

end;

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

then {x1,y} nin G by S3b, B4, D3, Lstable;
hence {x,y} nin Mycielskian G by A4, S3b, M0e4b; :: thesis: verum

end;

end;

end;

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

consider x1 being Element of union G such that
A4: x = [x1,(union G)] and
x1 in d by S3a, C3;
consider y1 being Element of union G such that
C4: y = [y1,(union G)] and
y1 in d by S3b, C3;
thus {x,y} nin Mycielskian G by A4, C4, A2, M0e3a; :: 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 B2, C2, TARSKI:def 1;
hence {x,y} nin Mycielskian G by A2; :: 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
A2: {(union G)} = d \/ (r . d) and
A2a: d in C ;
B2: union G in d \/ (r . d) by A2, TARSKI:def 1;

per cases ( union G in d or union G in r . d ) by B2, XBOOLE_0:def 3;

suppose union G in d ; :: thesis: contradiction

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

end;

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

then union G in { [x,(union G)] where x is Element of union G : x in d } by A2a, C;
then consider x being Element of union G such that
A3: union G = [x,(union G)] and
x in d ;
thus contradiction by A3, Aux2; :: thesis: verum

end;

end;

end;

hence card E = 1 + (chromatic# G) by D1, D1a, A, CARD_2:41; :: thesis: verum