for G being SimpleGraph
for x, y being set st y in union G & {[x,(union G)],y} in Mycielskian G holds
{x,y} in G