let G be with_finite_clique# SimpleGraph; ( clique# G = 1 implies for D being finite Clique of (Mycielskian G) holds order D <= 2 )
assume A1:
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 A2:
order D > 2
; contradiction
then A3:
order D >= 2 + 1
by NAT_1:13;
not union D is empty
by A2;
then consider v being object such that
A4:
v in union D
;
A5:
v <> union G
by A4, A3, Th105;
Segm 3 c= Segm (order D)
by A3, NAT_1:39;
then consider v1, v2 being object such that
A6:
v1 in union D
and
v2 in union D
and
A7:
v1 <> v
and
v2 <> v
and
v1 <> v2
by Th5;
A8:
v1 <> union G
by A6, A3, Th105;
set e = {v,v1};
{v,v1} in D
by A4, A6, Th53;
then A9:
{v,v1} in Edges (Mycielskian G)
by A7, Th12;
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 A9, Th90;
end;