let G be finitely_colorable SimpleGraph; 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 not 1 + (chromatic# G) > chromatic# (Mycielskian G)assume A3:
1
+ (chromatic# G) > chromatic# (Mycielskian G)
;
contradictionA4:
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 not EuG <> Ecseassume A23:
EuG <> Ecse
;
contradictionset sf =
Ecse /\ S;
A24:
Ecse meets S
by A21, A6, A7, A12, MYCIELSK:9;
A25:
Ecse /\ S in C
by A24, A21;
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;
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;
verum end;
hence
chromatic# (Mycielskian G) = 1 + (chromatic# G)
by A2, XXREAL_0:1; verum