let G be finitely_colorable SimpleGraph; :: thesis: chromatic# (Mycielskian G) = 1 + (chromatic# G)
set uG = union G;
set MG = Mycielskian G;
set uMG = union (Mycielskian G);
set cnG = chromatic# G;
set cnMG = chromatic# (Mycielskian G);
consider D being Coloring of (Mycielskian G) such that
A1: card D = 1 + (chromatic# G) by Th111;
D is finite by A1;
then A2: chromatic# (Mycielskian G) <= 1 + (chromatic# G) by A1, Def22;

now :: thesis: not 1 + (chromatic# G) > chromatic# (Mycielskian G)

assume A3: 1 + (chromatic# G) > chromatic# (Mycielskian G) ; :: thesis: contradiction
A4: chromatic# G >= chromatic# (Mycielskian G) by A3, NAT_1:13;
A5: chromatic# G <= chromatic# (Mycielskian G) by Th84, Th68;
A6: chromatic# G = chromatic# (Mycielskian G) by A4, A5, XXREAL_0:1;
consider E being finite Coloring of (Mycielskian G) such that
A7: card E = chromatic# (Mycielskian G) by Def22;
A8: union E = union (Mycielskian G) by EQREL_1:def 4;
A9: G = (Mycielskian G) SubgraphInducedBy (union G) by Th104;
reconsider S = union G as Subset of (Vertices (Mycielskian G)) by Th84, ZFMISC_1:77;
reconsider C = E | S as finite Coloring of G by A9, Th67;
A10: card C >= chromatic# G by Def22;
A11: card C <= chromatic# G by A6, A7, MYCIELSK:8;
A12: card C = chromatic# G by A10, A11, XXREAL_0:1;
A13: union G in union (Mycielskian G) by Th87;
then consider EuG being set such that
A14: union G in EuG and
A15: EuG in E by A8, TARSKI:def 4;
reconsider EuG = EuG as Subset of (Vertices (Mycielskian G)) by A15;
reconsider uG = union G as Element of Vertices (Mycielskian G) by A14, A15;
set se = EuG /\ S;
A16: EuG meets S by A15, A6, A7, A12, MYCIELSK:9;
EuG /\ S in C by A15, A16;
then consider sev being Element of Vertices G such that
A17: sev in EuG /\ S and
A18: for d being Element of C st d <> EuG /\ S holds
ex w being Element of Vertices G st
( w in Adjacent sev & w in d ) by A10, A11, Th70, XXREAL_0:1;
A19: not uG is empty by A16;
then {[sev,uG]} in Mycielskian G by Th95;
then reconsider csev = [sev,uG] as Element of Vertices (Mycielskian G) by Th24;
csev in Vertices (Mycielskian G) by A13;
then csev in union E by EQREL_1:def 4;
then consider Ecse being set such that
A20: csev in Ecse and
A21: Ecse in E by TARSKI:def 4;
reconsider Ecse = Ecse as Subset of (Vertices (Mycielskian G)) by A21;

A22: now :: thesis: not EuG <> Ecse

assume A23: EuG <> Ecse ; :: thesis: contradiction
set sf = Ecse /\ S;
A24: Ecse meets S by A21, A6, A7, A12, MYCIELSK:9;
A25: Ecse /\ S in C by A24, A21;

now :: thesis: not EuG /\ S = Ecse /\ S

assume EuG /\ S = Ecse /\ S ; :: thesis: contradiction
then ( sev in EuG & sev in Ecse ) by A17, XBOOLE_0:def 4;
then EuG meets Ecse by XBOOLE_0:3;
hence contradiction by A23, A21, A15, EQREL_1:def 4; :: thesis: verum

end;

then consider w being Element of Vertices G such that
A26: w in Adjacent sev and
A27: w in Ecse /\ S by A25, A18;
A28: w in Ecse by A27, XBOOLE_0:def 4;
A29: Ecse is stable by A21, Def20;
A30: csev <> w by A19, Th1;
{sev,w} in Edges G by A26, Def8;
then {csev,w} in Mycielskian G by Th102;
hence contradiction by A29, A30, A28, A20; :: thesis: verum

end;

A31: {csev,uG} in Edges (Mycielskian G) by A19, Th90;
A32: csev <> uG by Th2;
EuG is stable by A15, Def20;
hence contradiction by A32, A31, A22, A20, A14; :: thesis: verum

end;

hence chromatic# (Mycielskian G) = 1 + (chromatic# G) by A2, XXREAL_0:1; :: thesis: verum