let n be Nat; :: thesis:
let R be irreflexive NatRelStr of n; :: thesis:
set cR = the carrier of R;
set iR = the InternalRel of R;
set cnR = chromatic# R;
set MR = Mycielskian R;
set cnMR = chromatic# (Mycielskian R);
set cMR = the carrier of (Mycielskian R);
set iMR = the InternalRel of (Mycielskian R);
A: the carrier of R = n by LNRS;
Z1: ex C being finite Coloring of (Mycielskian R) st card C = 1 + (chromatic# R)

consider C being finite Coloring of R such that
A1: card C = chromatic# R by Lchro;
defpred S₁[ set , set ] means $2 = { (m + n) where m is Element of NAT : m in $1 } ;
P1: 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
C1: for e being set st e in C holds
S₁[e,r . e] from CLASSES1:sch 1(P1);
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

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

now

assume not C is empty ; :: thesis:
then consider c being set such that
A3: 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 A3;
hence contradiction by S2; :: thesis:

end;

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

end;

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

defpred S₂[ set , set ] means $2 = $1 \/ (r . $1);
R2: for e being set st e in C holds
ex u being set st S₂[e,u] ;
consider s being Function such that
B2: dom s = C and
C2: for e being set st e in C holds
S₂[e,s . e] from CLASSES1:sch 1(R2);
D2a: 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:
assume y in rng s ; :: thesis:
then consider x being set such that
A3: x in dom s and
B3: y = s . x by FUNCT_1:def 5;
y = x \/ (r . x) by A3, B3, B2, C2;
hence y in { (d \/ (r . d)) where d is Element of C : d in C } by A3, B2; :: thesis:

end;

then reconsider s = s as Function of C, { (d \/ (r . d)) where d is Element of C : d in C } by B2, FUNCT_2:4;
{ (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:
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
A3: x = c \/ (r . c) and
B3: c in C ;
x = s . c by A3, B3, C2;
hence x in rng s by B3, B2, FUNCT_1:def 5; :: thesis:

end;

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

proof

let x1, x2 be set ; :: according to FUNCT_1:def 8 :: thesis:
assume that
A3: x1 in dom s and
B3: x2 in dom s and
C3: s . x1 = s . x2 ; :: thesis:
D3: s . x1 = x1 \/ (r . x1) by A3, C2;
E3: s . x2 = x2 \/ (r . x2) by B3, C2;
thus x1 c= x2 :: according to XBOOLE_0:def 10 :: thesis:

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A4: x in x1 ; :: thesis:
B4: x in s . x1 by D3, A4, XBOOLE_0:def 3;

per cases by B4, C3, E3, XBOOLE_0:def 3;

suppose x in x2 ; :: thesis:

hence x in x2 ; :: thesis:

end;

suppose x in r . x2 ; :: thesis:

then x in { (m + n) where m is Element of NAT : m in x2 } by C1, B3;
then consider m being Element of NAT such that
A5: x = m + n and
m in x2 ;
m + n < 0 + n by A4, A5, A3, B2, A, NAT_1:45;
hence x in x2 by XREAL_1:8; :: thesis:

end;

thus x2 c= x1 :: thesis:

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A4: x in x2 ; :: thesis:
B4: x in s . x2 by E3, A4, XBOOLE_0:def 3;

per cases by B4, C3, D3, XBOOLE_0:def 3;

suppose x in x1 ; :: thesis:

hence x in x1 ; :: thesis:

end;

suppose x in r . x1 ; :: thesis:

then x in { (m + n) where m is Element of NAT : m in x1 } by C1, A3;
then consider m being Element of NAT such that
A5: x = m + n and
m in x1 ;
m + n < 0 + n by A4, A5, B3, B2, A, NAT_1:45;
hence x in x1 by XREAL_1:8; :: thesis:

end;

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

end;

then D1a: { (d \/ (r . d)) where d is Element of C : d in C } is finite ;
set E = { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}};
F1a: union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}}) c= the carrier of (Mycielskian R)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}}) ; :: thesis:
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 } \/ {{(2 * n)}} by TARSKI:def 4;

per cases by B2, 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
A3: Y = d \/ (r . d) and
B3: d in C ;
D3: r . d = { (m + n) where m is Element of NAT : m in d } by B3, C1;

per cases by A2, A3, XBOOLE_0:def 3;

suppose A2a: x in d ; :: thesis:

reconsider a = x as Nat by A2a, B3, A, NECKLACE:4;
a < n by A2a, B3, A, NAT_1:45;
then a + 0 < n + n by XREAL_1:10;
then a < (2 * n) + 1 by NAT_1:13;
then a in (2 * n) + 1 by NAT_1:45;
hence x in the carrier of (Mycielskian R) by LNRS; :: thesis:

end;

suppose x in r . d ; :: thesis:

then consider m being Element of NAT such that
A2: x = m + n and
B2: m in d by D3;
m < n by B2, B3, A, NAT_1:45;
then m + n < n + n by XREAL_1:8;
then m + n < (2 * n) + 1 by NAT_1:13;
then x in (2 * n) + 1 by A2, NAT_1:45;
hence x in the carrier of (Mycielskian R) by LNRS; :: thesis:

end;

suppose Y in {{(2 * n)}} ; :: thesis:

then Y = {(2 * n)} by TARSKI:def 1;
then B2: x = 2 * n by A2, TARSKI:def 1;
2 * n < (2 * n) + 1 by NAT_1:13;
then 2 * n in (2 * n) + 1 by NAT_1:45;
hence x in the carrier of (Mycielskian R) by B2, LNRS; :: thesis:

end;

E1: { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}} c= bool the carrier of (Mycielskian R)

proof

let X be set ; :: according to TARSKI:def 3 :: thesis:
assume A2: X in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}} ; :: thesis:
X c= the carrier of (Mycielskian R)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in X ; :: thesis:
then x in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}}) by A2, TARSKI:def 4;
hence x in the carrier of (Mycielskian R) by F1a; :: thesis:

end;

hence X in bool the carrier of (Mycielskian R) ; :: thesis:

end;

F1: union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}}) = the carrier of (Mycielskian R)

proof

thus union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}}) c= the carrier of (Mycielskian R) by F1a; :: according to XBOOLE_0:def 10 :: thesis:
thus the carrier of (Mycielskian R) c= union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}}) :: thesis:

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in the carrier of (Mycielskian R) ; :: thesis:
then A2: x in (2 * n) + 1 by LNRS;
then reconsider a = x as Nat by NECKLACE:4;
a < (2 * n) + 1 by A2, NAT_1:45;
then B2: a <= 2 * n by NAT_1:13;

per cases ;

suppose a < n ; :: thesis:

then a in n by NAT_1:45;
then a in union C by A, EQREL_1:def 6;
then consider c being set such that
B2: a in c and
C2: c in C by TARSKI:def 4;
D2: x in c \/ (r . c) by B2, XBOOLE_0:def 3;
c \/ (r . c) in { (d \/ (r . d)) where d is Element of C : d in C } by C2;
then c \/ (r . c) in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}} by XBOOLE_0:def 3;
hence x in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}}) by D2, TARSKI:def 4; :: thesis:

end;

suppose S1: a >= n ; :: thesis:

per cases by B2, XXREAL_0:1;

suppose S2: a < n + n ; :: thesis:

consider b being Nat such that
A2: a = n + b by S1, NAT_1:10;
reconsider b = b as Element of NAT by ORDINAL1:def 13;
b < n by A2, S2, XREAL_1:8;
then b in the carrier of R by A, NAT_1:45;
then b in union C by EQREL_1:def 6;
then consider c being set such that
B2: b in c and
C2: c in C by TARSKI:def 4;
r . c = { (m + n) where m is Element of NAT : m in c } by C2, C1;
then a in r . c by B2, A2;
then D2: x in c \/ (r . c) by XBOOLE_0:def 3;
c \/ (r . c) in { (d \/ (r . d)) where d is Element of C : d in C } by C2;
then c \/ (r . c) in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}} by XBOOLE_0:def 3;
hence x in union ( { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}}) by D2, TARSKI:def 4; :: thesis:

end;

suppose a = 2 * n ; :: thesis:

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

end;

now

let A be Subset of the carrier of (Mycielskian R); :: thesis:
assume A2: A in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}} ; :: thesis:
thus A <> {} :: thesis:

proof

per cases by A2, 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
A3: A = d \/ (r . d) and
B3: d in C ;
d <> {} by B3, EQREL_1:def 6;
hence A <> {} by A3; :: thesis:

end;

suppose A in {{(2 * n)}} ; :: thesis:

hence A <> {} by TARSKI:def 1; :: thesis:

end;

let B be Subset of the carrier of (Mycielskian R); :: thesis:
assume B2: B in { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}} ; :: thesis:
assume C2: A <> B ; :: thesis:
assume A meets B ; :: thesis:
then consider x being set such that
D2: x in A and
E2: x in B by XBOOLE_0:3;

per cases by A2, B2, XBOOLE_0:def 3;

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

consider d being Element of C such that
C3a: A = d \/ (r . d) and
D3a: d in C by S1a;
consider e being Element of C such that
C3b: B = e \/ (r . e) and
D3b: e in C by S1b;

per cases by C3a, C3b, D2, E2, XBOOLE_0:def 3;

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

then d meets e by XBOOLE_0:3;
then d = e by D3a, D3b, EQREL_1:def 6;
hence contradiction by C3a, C3b, C2; :: thesis:

end;

suppose that S2a: x in d and
S2b: x in r . e ; :: thesis:

x in { (m + n) where m is Element of NAT : m in e } by S2b, D3b, C1;
then consider mb being Element of NAT such that
A4a: x = mb + n and
mb in e ;
mb + n < n + 0 by A4a, S2a, D3a, A, NAT_1:45;
hence contradiction by XREAL_1:8; :: thesis:

end;

suppose that S2a: x in r . d and
S2b: x in e ; :: thesis:

x in { (m + n) where m is Element of NAT : m in d } by S2a, D3a, C1;
then consider ma being Element of NAT such that
A4a: x = ma + n and
ma in d ;
ma + n < n + 0 by A4a, S2b, D3b, A, NAT_1:45;
hence contradiction by XREAL_1:8; :: thesis:

end;

suppose that S2a: x in r . d and
S2b: x in r . e ; :: thesis:

x in { (m + n) where m is Element of NAT : m in d } by S2a, D3a, C1;
then consider ma being Element of NAT such that
A4a: x = ma + n and
B4a: ma in d ;
x in { (m + n) where m is Element of NAT : m in e } by S2b, D3b, C1;
then consider mb being Element of NAT such that
A4b: x = mb + n and
B4b: mb in e ;
d meets e by A4a, A4b, B4a, B4b, XBOOLE_0:3;
then d = e by D3a, D3b, EQREL_1:def 6;
hence contradiction by C3a, C3b, C2; :: thesis:

end;

suppose that S1a: A in { (d \/ (r . d)) where d is Element of C : d in C } and
S1b: B in {{(2 * n)}} ; :: thesis:

B = {(2 * n)} by S1b, TARSKI:def 1;
then B3: x = 2 * n by E2, TARSKI:def 1;
consider d being Element of C such that
C3: A = d \/ (r . d) and
D3: d in C by S1a;

per cases by C3, D2, XBOOLE_0:def 3;

suppose x in d ; :: thesis:

then n + n < n by D3, A, B3, NAT_1:45;
hence contradiction by NAT_1:11; :: thesis:

end;

suppose x in r . d ; :: thesis:

then x in { (m + n) where m is Element of NAT : m in d } by D3, C1;
then consider m being Element of NAT such that
A4: x = m + n and
B4: m in d ;
m in n by B4, D3, A;
hence contradiction by A4, B3; :: thesis:

end;

suppose that S1a: A in {{(2 * n)}} and
S1b: B in { (d \/ (r . d)) where d is Element of C : d in C } ; :: thesis:

A = {(2 * n)} by S1a, TARSKI:def 1;
then B3: x = 2 * n by D2, TARSKI:def 1;
consider d being Element of C such that
C3: B = d \/ (r . d) and
D3: d in C by S1b;

per cases by C3, E2, XBOOLE_0:def 3;

suppose x in d ; :: thesis:

then n + n < n by D3, A, B3, NAT_1:45;
hence contradiction by NAT_1:11; :: thesis:

end;

suppose x in r . d ; :: thesis:

end;

suppose ( A in {{(2 * n)}} & B in {{(2 * n)}} ) ; :: thesis:

then ( A = {(2 * n)} & B = {(2 * n)} ) by TARSKI:def 1;
hence contradiction by C2; :: thesis:

end;

then reconsider E = { (d \/ (r . d)) where d is Element of C : d in C } \/ {{(2 * n)}} as a_partition of the carrier of (Mycielskian R) by E1, F1, EQREL_1:def 6;

now

let x be set ; :: thesis:
assume A2: x in E ; :: thesis:

per cases by A2, 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
A3: x = d \/ (r . d) and
B3: d in C ;
reconsider d = d as Subset of R by B3;
D3: r . d = { (m + n) where m is Element of NAT : m in d } by B3, C1;
C3: x c= the carrier of (Mycielskian R)

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume A4: a in x ; :: thesis:

per cases by A3, A4, XBOOLE_0:def 3;

suppose S5: a in d ; :: thesis:

then reconsider ap1 = a as Nat by A, NECKLACE:4;
B5: ap1 < n by S5, A, NAT_1:45;
n <= n + n by NAT_1:12;
then ap1 < n + n by B5, XXREAL_0:2;
then ap1 < (2 * n) + 1 by NAT_1:13;
then a in (2 * n) + 1 by NAT_1:45;
hence a in the carrier of (Mycielskian R) by LNRS; :: thesis:

end;

suppose a in r . d ; :: thesis:

then consider am being Element of NAT such that
B5: a = am + n and
C5: am in d by D3;
am < n by C5, A, NAT_1:45;
then am + n < n + n by XREAL_1:8;
then am + n < (2 * n) + 1 by NAT_1:13;
then a in (2 * n) + 1 by B5, NAT_1:45;
hence a in the carrier of (Mycielskian R) by LNRS; :: thesis:

end;

A2e: now

let x be Nat; :: thesis:
assume x in r . d ; :: thesis:
then consider m being Element of NAT such that
A3: x = m + n and
B3: m in d by D3;
thus n <= x by A3, NAT_1:11; :: thesis:
m < n by NAT_1:45, B3, A;
then m + n < n + n by XREAL_1:8;
hence x < 2 * n by A3; :: thesis:

end;

A2f: d is stable by B3, DILWORTH:def 12;

now

let a, b be Element of (Mycielskian R); :: thesis:
assume that
A4: a in x and
B4: b in x and
C4: a <> b and
D4: ( a <= b or b <= a ) ; :: thesis:
D4a: ( [a,b] in the InternalRel of (Mycielskian R) or [b,a] in the InternalRel of (Mycielskian R) ) by D4, ORDERS_2:def 9;

per cases by A4, B4, A3, XBOOLE_0:def 3;

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

then B5: ( [a,b] in the InternalRel of R or [b,a] in the InternalRel of R ) by A, D4a, iMR1b;
reconsider a = a, b = b as Element of R by S5;
( a <= b or b <= a ) by B5, ORDERS_2:def 9;
hence contradiction by S5, C4, A2f, DILWORTH:def 2; :: thesis:

end;

suppose that S5a: a in d and
S5b: b in r . d ; :: thesis:

consider bm being Element of NAT such that
B5: b = bm + n and
C5: bm in d by S5b, D3;
reconsider ap1 = a as Nat by S5a, A, NECKLACE:4;
D5: ( [ap1,bm] in the InternalRel of R or [bm,ap1] in the InternalRel of R ) by D4a, iMR1c, iMR1d, B5, S5a, A;
reconsider bmp1 = bm, a = a as Element of R by C5, S5a;
E5: ( bmp1 <= a or a <= bmp1 ) by D5, ORDERS_2:def 9;
bmp1 <> a by D5, S5a, NECKLACE:def 6;
hence contradiction by E5, C5, S5a, A2f, DILWORTH:def 2; :: thesis:

end;

suppose that S5a: a in r . d and
S5b: b in d ; :: thesis:

consider am being Element of NAT such that
B5: a = am + n and
C5: am in d by S5a, D3;
reconsider bp1 = b as Nat by S5b, A, NECKLACE:4;
D5: ( [am,bp1] in the InternalRel of R or [bp1,am] in the InternalRel of R ) by D4a, iMR1c, iMR1d, B5, S5b, A;
reconsider amp1 = am, b = b as Element of R by C5, S5b;
E5: ( amp1 <= b or b <= amp1 ) by D5, ORDERS_2:def 9;
amp1 <> b by D5, S5b, NECKLACE:def 6;
hence contradiction by E5, C5, S5b, A2f, DILWORTH:def 2; :: thesis:

end;

suppose that S5a: a in r . d and
S5b: b in r . d ; :: thesis:

consider am being Element of NAT such that
B5: a = am + n and
am in d by S5a, D3;
consider bm being Element of NAT such that
D5: b = bm + n and
bm in d by S5b, D3;
( n <= am + n & am + n < 2 * n & n <= bm + n & bm + n < 2 * n ) by S5a, S5b, B5, D5, A2e;
hence contradiction by B5, D5, D4a, iMR0; :: thesis:

end;

hence x is StableSet of (Mycielskian R) by C3, DILWORTH:def 2; :: thesis:

end;

suppose x in {{(2 * n)}} ; :: thesis:

then S2: x = {(2 * n)} by TARSKI:def 1;
2 * n < (2 * n) + 1 by NAT_1:13;
then 2 * n in (2 * n) + 1 by NAT_1:45;
then A3: 2 * n in the carrier of (Mycielskian R) by LNRS;
x is Subset of (Mycielskian R) by S2, A3, SUBSET_1:55;
hence x is StableSet of (Mycielskian R) by S2; :: thesis:

end;

then reconsider E = E as Coloring of (Mycielskian R) by DILWORTH:def 12;
take E ; :: thesis:

now

assume {(2 * n)} in { (d \/ (r . d)) where d is Element of C : d in C } ; :: thesis:
then consider d being Element of C such that
A2: {(2 * n)} = d \/ (r . d) and
A2a: d in C ;
B2: 2 * n in d \/ (r . d) by A2, TARSKI:def 1;

per cases by B2, XBOOLE_0:def 3;

suppose 2 * n in d ; :: thesis:

then 2 * n in the carrier of R by A2a;
then 2 * n in n by LNRS;
then n + n < n by NAT_1:45;
hence contradiction by NAT_1:11; :: thesis:

end;

suppose 2 * n in r . d ; :: thesis:

then 2 * n in { (m + n) where m is Element of NAT : m in d } by A2a, C1;
then consider m being Element of NAT such that
A3: 2 * n = m + n and
B3: m in d ;
m in the carrier of R by A2a, B3;
then m in n by LNRS;
hence contradiction by A3; :: thesis:

end;

hence card E = 1 + (chromatic# R) by D1, D1a, A1, CARD_2:54; :: thesis:

end;

for C being finite Coloring of (Mycielskian R) holds 1 + (chromatic# R) <= card C

proof

let E be finite Coloring of (Mycielskian R); :: thesis:
assume 1 + (chromatic# R) > card E ; :: thesis:
then A1: chromatic# R >= card E by NAT_1:13;
A1a: chromatic# (Mycielskian R) <= card E by Lchro;
then B1: chromatic# (Mycielskian R) <= chromatic# R by A1, XXREAL_0:2;
n <= n + n by NAT_1:11;
then n < (2 * n) + 1 by NAT_1:13;
then n c= (2 * n) + 1 by NAT_1:40;
then reconsider S = n as Subset of (Mycielskian R) by LNRS;
C1: R = subrelstr S by Msubrel;
then chromatic# R <= chromatic# (Mycielskian R) by Tchro0;
then chromatic# R = chromatic# (Mycielskian R) by B1, XXREAL_0:1;
then D1a: card E = chromatic# R by A1, A1a, XXREAL_0:1;
reconsider C = E | S as Coloring of R by C1, Tsr0;
E1: card C >= chromatic# R by Lchro;
F1a: card C <= card E by Tpart0;
then F1: card C = chromatic# R by D1a, E1, XXREAL_0:1;
2 * n < (2 * n) + 1 by NAT_1:13;
then 2 * n in (2 * n) + 1 by NAT_1:45;
then 2 * n in the carrier of (Mycielskian R) by LNRS;
then 2 * n in union E by EQREL_1:def 6;
then consider e being set such that
K1a: 2 * n in e and
K1b: e in E by TARSKI:def 4;
reconsider e = e as Subset of (Mycielskian R) by K1b;
reconsider n2 = 2 * n as Element of (Mycielskian R) by K1a, K1b;
set se = e /\ S;
e meets S by D1a, F1, K1b, Tpart1;
then L1: e /\ S in C by K1b;
then consider mp1 being Element of R such that
L1a: mp1 in e /\ S and
H1: for d being Element of C st d <> e /\ S holds
ex w being Element of R st
( w in Adjacent mp1 & w in d ) by F1a, D1a, E1, XXREAL_0:1, AdjCol;
reconsider m = mp1 as Nat by L1a, L1, NECKLACE:4;
set mn = m + n;
L1cc: 0 + n <= m + n by XREAL_1:8;
m < n by L1a, L1, NAT_1:45;
then L1c: m + n < n + n by XREAL_1:8;
then m + n < (2 * n) + 1 by NAT_1:13;
then L1dd: m + n in (2 * n) + 1 by NAT_1:45;
then m + n in the carrier of (Mycielskian R) by LNRS;
then m + n in union E by EQREL_1:def 6;
then consider f being set such that
M1a: m + n in f and
M1b: f in E by TARSKI:def 4;
reconsider f = f as Subset of (Mycielskian R) by M1b;
reconsider mnp1 = m + n as Element of (Mycielskian R) by L1dd, LNRS;

M: now

assume A2: e <> f ; :: thesis:
set sf = f /\ S;
f meets S by D1a, F1, M1b, Tpart1;
then B2: f /\ S in C by M1b;
B2a: f /\ S c= f by XBOOLE_1:17;

now

assume A3: f /\ S = e /\ S ; :: thesis:
f /\ S <> {} by B2, EQREL_1:def 6;
then consider x being set such that
B3: x in f /\ S by XBOOLE_0:def 1;
e /\ S c= e by XBOOLE_1:17;
then e meets f by A3, B3, B2a, XBOOLE_0:3;
hence contradiction by A2, M1b, K1b, EQREL_1:def 6; :: thesis:

end;

then consider wp1 being Element of R such that
D2: wp1 in Adjacent mp1 and
E2: wp1 in f /\ S by B2, H1;
reconsider w = wp1 as Nat by E2, B2, NECKLACE:4;
G2: w < n by E2, B2, NAT_1:45;
( mp1 < wp1 or wp1 < mp1 ) by D2, LAdjset;
then ( mp1 <= wp1 or wp1 <= mp1 ) by ORDERS_2:def 10;
then ( [m,w] in the InternalRel of R or [w,m] in the InternalRel of R ) by ORDERS_2:def 9;
then H2: ( [(m + n),w] in the InternalRel of (Mycielskian R) or [w,(m + n)] in the InternalRel of (Mycielskian R) ) by iMR1a;
reconsider wp2 = wp1 as Element of (Mycielskian R) by E2;
f is stable by M1b, DILWORTH:def 12;
then ( not wp2 <= mnp1 & not mnp1 <= wp2 ) by G2, L1cc, E2, B2a, M1a, DILWORTH:def 2;
hence contradiction by H2, ORDERS_2:def 9; :: thesis:

end;

N: [(m + n),(2 * n)] in the InternalRel of (Mycielskian R) by L1c, L1cc, iMR1e;
e is stable by K1b, DILWORTH:def 12;
then ( not mnp1 <= n2 & not n2 <= mnp1 ) by K1a, M1a, M, L1c, DILWORTH:def 2;
hence contradiction by N, ORDERS_2:def 9; :: thesis:

end;

hence chromatic# (Mycielskian R) = 1 + (chromatic# R) by Z1, Lchro; :: thesis: