set MG = Mycielskian G;
set uG = union G;
per cases
( clique# G = 0 or clique# G = 1 or clique# G > 1 )
by NAT_1:25;
suppose A3:
clique# G = 1
;
Mycielskian G is with_finite_clique# then consider C being
finite Clique of
G such that A4:
order C = 1
by Def15;
A5:
union C c= union G
by ZFMISC_1:77;
Vertices C <> {}
by A4;
then consider v being
object such that A6:
v in Vertices C
by XBOOLE_0:def 1;
A7:
[v,(union G)] in union (Mycielskian G)
by A6, A5, Th85;
A8:
union G in union (Mycielskian G)
by Th87;
A9:
{[v,(union G)],(union G)} in Mycielskian G
by A6, A5, Th96;
reconsider CC =
{{},{[v,(union G)]},{(union G)},{[v,(union G)],(union G)}} as
finite Clique of
(Mycielskian G) by A7, A8, A9, Th51;
A10:
CC = CompleteSGraph {[v,(union G)],(union G)}
by Th37;
A11:
Vertices CC = {[v,(union G)],(union G)}
by A10, Lm1;
take
CC
;
SCMYCIEL:def 14 for D being finite Clique of (Mycielskian G) holds order D <= order CC
order CC = 2
by A11, Th2, CARD_2:57;
hence
for
D being
finite Clique of
(Mycielskian G) holds
order D <= order CC
by A3, Th108;
verum end;