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
A: card D = 1 + (chromatic# G) by Mfc1;
D is finite by A;
then Z: chromatic# (Mycielskian G) <= 1 + (chromatic# G) by A, Lchro;

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

assume A1: 1 + (chromatic# G) > chromatic# (Mycielskian G) ; :: thesis: contradiction
B1: chromatic# G >= chromatic# (Mycielskian G) by A1, NAT_1:13;
C1: chromatic# G <= chromatic# (Mycielskian G) by M0, Subchro;
D1: chromatic# G = chromatic# (Mycielskian G) by B1, C1, XXREAL_0:1;
consider E being finite Coloring of (Mycielskian G) such that
E1: card E = chromatic# (Mycielskian G) by Lchro;
E1a: union E = union (Mycielskian G) by EQREL_1:def 4;
EE: G = (Mycielskian G) SubgraphInducedBy (union G) by GsubMG;
reconsider S = union G as Subset of (Vertices (Mycielskian G)) by M0, ZFMISC_1:77;
reconsider C = E | S as finite Coloring of G by EE, Tsr0;
F1: card C >= chromatic# G by Lchro;
G1: card C <= chromatic# G by D1, E1, MYCIELSK:8;
H1: card C = chromatic# G by F1, G1, XXREAL_0:1;
H1a: union G in union (Mycielskian G) by M00;
then consider EuG being set such that
I1: union G in EuG and
J1: EuG in E by E1a, TARSKI:def 4;
reconsider EuG = EuG as Subset of (Vertices (Mycielskian G)) by J1;
reconsider uG = union G as Element of Vertices (Mycielskian G) by I1, J1;
set se = EuG /\ S;
K1: EuG meets S by J1, D1, E1, H1, MYCIELSK:9;
EuG /\ S in C by J1, K1;
then consider sev being Element of Vertices G such that
M1: sev in EuG /\ S and
N1: 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 F1, G1, XXREAL_0:1, AdjCol;
N1a: not uG is empty by XBOOLE_1:65, K1;
then {[sev,uG]} in Mycielskian G by M0e2aa;
then reconsider csev = [sev,uG] as Element of Vertices (Mycielskian G) by Vertices0;
csev in Vertices (Mycielskian G) by H1a;
then csev in union E by EQREL_1:def 4;
then consider Ecse being set such that
O1: csev in Ecse and
P1: Ecse in E by TARSKI:def 4;
reconsider Ecse = Ecse as Subset of (Vertices (Mycielskian G)) by P1;

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

assume A2: EuG <> Ecse ; :: thesis: contradiction
set sf = Ecse /\ S;
B2: Ecse meets S by P1, D1, E1, H1, MYCIELSK:9;
C2: Ecse /\ S in C by B2, P1;

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

assume EuG /\ S = Ecse /\ S ; :: thesis: contradiction
then ( sev in EuG & sev in Ecse ) by M1, XBOOLE_0:def 4;
then EuG meets Ecse by XBOOLE_0:3;
hence contradiction by A2, P1, J1, EQREL_1:def 4; :: thesis: verum

end;

then consider w being Element of Vertices G such that
D2: w in Adjacent sev and
E2: w in Ecse /\ S by C2, N1;
F2: w in Ecse by E2, XBOOLE_0:def 4;
G2: Ecse is stable by P1, LStableSetwise;
H2: csev <> w by N1a, Aux1;
{sev,w} in Edges G by D2, Ladj;
then {csev,w} in Mycielskian G by M0e4c;
hence contradiction by G2, H2, F2, O1, Lstable; :: thesis: verum

end;

R1a: {csev,uG} in Edges (Mycielskian G) by N1a, M0e0;
S1: csev <> uG by Aux2;
EuG is stable by J1, LStableSetwise;
hence contradiction by S1, R1a, Q1, O1, I1, Lstable; :: thesis: verum

end;

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