for G being SimpleGraph
for u being object st u in Vertices G holds
{[u,(union G)]} in Mycielskian G