for G being SimpleGraph
for C being finite Clique of (Mycielskian G) st 3 <= order C holds
for v being Vertex of C holds v <> union G