let G be SimpleGraph; for C being finite Clique of (Mycielskian G) st 3 <= order C holds
for v being Vertex of C holds v <> union G
let C be finite Clique of (Mycielskian G); ( 3 <= order C implies for v being Vertex of C holds v <> union G )
assume A1:
3 <= order C
; for v being Vertex of C holds v <> union G
set MG = Mycielskian G;
let v be Vertex of C; v <> union G
assume A2:
v = union G
; contradiction
Segm 3 c= Segm (order C)
by A1, NAT_1:39;
then consider v1, v2 being object such that
A3:
v1 in Vertices C
and
A4:
v2 in Vertices C
and
A5:
v1 <> v
and
A6:
v2 <> v
and
A7:
v1 <> v2
by Th5;
A8:
{v,v1} in C
by A3, Th53;
A9:
{v,v2} in C
by A4, Th53;
A10:
{v,v1} in Edges (Mycielskian G)
by A8, A5, Th12;
A11:
{v,v2} in Edges (Mycielskian G)
by A6, A9, Th12;
consider x1 being object such that
x1 in union G
and
A12:
v1 = [x1,(union G)]
by A2, A10, Th94;
consider x2 being object such that
x2 in union G
and
A13:
v2 = [x2,(union G)]
by A2, A11, Th94;
{v1,v2} in C
by A3, A4, Th53;
hence
contradiction
by A12, A13, A7, Th98; verum