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 A:
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 B:
v = union G
; contradiction
3 c= order C
by A, NAT_1:39;
then consider v1, v2 being set such that
D:
v1 in Vertices C
and
E:
v2 in Vertices C
and
F:
v1 <> v
and
G:
v2 <> v
and
H:
v1 <> v2
by card3;
Ia:
{v,v1} in C
by D, Clique2a;
Ja:
{v,v2} in C
by E, Clique2a;
I1:
{v,v1} in Edges (Mycielskian G)
by Ia, F, SG4a;
J1:
{v,v2} in Edges (Mycielskian G)
by G, Ja, SG4a;
consider x1 being set such that
x1 in union G
and
Kb:
v1 = [x1,(union G)]
by B, I1, M0e2;
consider x2 being set such that
x2 in union G
and
Lb:
v2 = [x2,(union G)]
by B, J1, M0e2;
{v1,v2} in C
by D, E, Clique2a;
hence
contradiction
by Kb, Lb, H, M0e3a; verum