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 S1:
clique# G = 1
;
Mycielskian G is with_finite_clique# then consider C being
finite Clique of
G such that A1:
order C = 1
by Lcliqueno;
A1b:
union C c= union G
by ZFMISC_1:77;
Vertices C <> {}
by A1;
then consider v being
set such that B1:
v in Vertices C
by XBOOLE_0:def 1;
C1:
[v,(union G)] in union (Mycielskian G)
by B1, A1b, M0v1;
D1:
union G in union (Mycielskian G)
by M00;
E1:
{[v,(union G)],(union G)} in Mycielskian G
by B1, A1b, M0e2a;
reconsider CC =
{{},{[v,(union G)]},{(union G)},{[v,(union G)],(union G)}} as
finite Clique of
(Mycielskian G) by C1, D1, E1, Cliqueon2;
B1a:
CC = CompleteSGraph {[v,(union G)],(union G)}
by P2;
B1d:
Vertices CC = {[v,(union G)],(union G)}
by B1a, CSGLem1;
take
CC
;
SCMYCIEL:def 14 for D being finite Clique of (Mycielskian G) holds order D <= order CC
order CC = 2
by B1d, Aux2, CARD_2:57;
hence
for
D being
finite Clique of
(Mycielskian G) holds
order D <= order CC
by S1, MClique1;
verum end;