let G be with_finite_clique# SimpleGraph; ( clique# G = 1 implies for D being finite Clique of (Mycielskian G) holds order D <= 2 )
assume A:
clique# G = 1
; for D being finite Clique of (Mycielskian G) holds order D <= 2
set uG = union G;
set MG = Mycielskian G;
set uMG = union (Mycielskian G);
let D be finite Clique of (Mycielskian G); order D <= 2
set uD = union D;
assume H0:
order D > 2
; contradiction
then H:
order D >= 2 + 1
by NAT_1:13;
not union D is empty
by H0;
then consider v being set such that
A0:
v in union D
by XBOOLE_0:def 1;
C:
v <> union G
by A0, H, MClique3;
3 c= order D
by H, NAT_1:39;
then consider v1, v2 being set such that
B1:
v1 in union D
and
v2 in union D
and
B3:
v1 <> v
and
v2 <> v
and
v1 <> v2
by card3;
C1:
v1 <> union G
by B1, H, MClique3;
set e = {v,v1};
{v,v1} in D
by A0, B1, Clique2a;
then F0:
{v,v1} in Edges (Mycielskian G)
by B3, SG4a;
per cases
( {v,v1} in Edges G or ex x, y being Element of union G st
( {v,v1} = {x,[y,(union G)]} & {x,y} in Edges G ) or ex y being Element of union G st
( {v,v1} = {(union G),[y,(union G)]} & y in union G ) )
by F0, M0e0;
end;